This project addresses the problem of efficiently calculating a logically correct supervisor for reactive systems. The work is oriented towards design of computer algorithms in a formal mathematical way, mathematically proving their correctness. Straight-forward approaches stumble on an inherent complexity problem known as the state-space explosion problem. This problem also makes manual design of supervisors intractable for all but rather small systems, due to the overwhelming complexity.
Supervisor synthesis is a formal approach to designing correct manufacturing systems control, embedded systems functionality and similar types of "reactive" systems. These have in common that they are safety-critical, and a supervisor is a safety-device that assures that the supervised system does not break the given specifications. This logical correctness is crucial for human safety when interacting with these types of systems.
The research focuses on compositional abstraction-based synthesis approaches, which try to exploit the inherent modular structure of the system by incrementally replacing system components with components of smaller size but with equal synthesis properties, until the original synthesis problem is modified into an equivalent problem of tractable size. Synthesizing a supervisor for the smaller version is guaranteed to generate a supervisor appropriate also for the, generally much larger, original problem.
The research is conducted in collaboration with Professor Robi Malik, University of Waikato, Hamilton, New Zealand.