Reactive synthesis and supervisory control theory both provide a design methodology for the automatic and algorithmic design of digital systems from declarative specifications. The reactive synthesis approach originates in computer science, and seeks to synthesize a system that interacts with its environment over time and that, doing so, satisfies a prescribed specification. Supervisory control originates in control theory and seeks to synthesize a controller that – in closed-loop configuration with a plant – enforces a prescribed specification over time. While both methods apparently are closely related, the technical details differ significantly.

Our research aims at understanding the fundamental connection between both disciplines to enable fruitful collaborations between the discrete control and the computer science community in the context of reliable CPS design.

Group Members Involved:

• Anne-Kathrin Schmuck

Collaborators:

• Rupak Majumdar (MPI-SWS)
• Thomas Moor (FAU, Erlangen, Germany)
• Nir Piterman (Chalmers)
• Klaus Schmidt (Ankara, Turkey)

Publications:

• A conceptual bridge for non-terminating processes
  • with Rupak Majumdar (MPI-SWS) and Thomas Moor (Erlangen)
  • [JDES’20], [TAC’23]
• Using ideas from symbolic game solving algorithms to improve supervisor synthesis
  • with Thomas Moor (Erlangen) and Klaus Schmidt (Ankara, Turkey)
  • [IFAC-WC’20a] [IFAC-WC’20b]
• Using ideas from supervisory control to improve reactive synthesis under environment assumptions
  • with Nir Piterman (Chalmers)
  • [TACAS’19], [TechReport]