Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Reactive Synthesis vs. Supervisory Control: Bridging the Gap

PIs: Lafortune (Michigan), Tripakis (Berkeley) and Vardi (Rice)

This work aims to establish a formal connection between synthesis problems that have been considered, largely separately, in the two research communities of control engineering and formal methods. By making this connection mathematically precise, we aim to bridge the gap between two research areas that tackle similar synthesis problems, but from different angles, and by emphasizing different, and often complementary, aspects. Such a formal bridge will be a source of inspiration for new lines of investigation that will leverage the power of the synthesis techniques that have been developed in these two areas. These results cover synthesis problems under full observation and partial controllability [ELSV14]. Current efforts are aimed at extending the bridge to synthesis problems in the context of partial observation.

Another aspect of this work concerns the development of a new methodology for the synthesis of safe and non-blocking supervisors for partially-observed discrete-event systems. This methodology is based on the construction of a new structure called the “All Inclusive Controller” (AIC), which is a bipartite transition system that embeds all safe and non-blocking supervisors and thus all controllable and observable solutions to the problem. We have developed a methodology that employs the AIC to synthesize supervisors that provably possess a desired maximality property; this was a long-standing open problem in supervisory control. These new results are applicable to the synthesis of supervisors for a wide class of real world cyber-physical systems with partial observations [YL14].


Papers:

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996