Supervisory Controller Synthesis for Non-terminating Processes is an Obliging Game

2020/07/03 by Rupak Majumdar, Anne-Kathrin Schmuck, Majumdar, Rupak +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Petri Nets in System Modeling #Systems and Control (eess.SY) #electronic engineering #information engineering

paper · pdf · doi:10.48550/arxiv.2007.01773

openalex publication_date 2020/07/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We present a new algorithm to solve the supervisory control problem over non-terminating processes modeled as ω-regular automata. A solution to this problem was obtained by Thistle in 1995 which uses complex manipulations of automata. We show a new solution to the problem through a reduction to obliging games, which, in turn, can be reduced to ω-regular reactive synthesis. Therefore, our reduction results in a symbolic algorithm based on manipulating sets of states using tools from reactive synthesis.

Cited by

• Scaling GR(1) Synthesis via a Compositional Framework for LTL Discrete Event Control

Related

• Reactive Supervisory Control of Open Discrete-event Systems
• Supervisory Control Synthesis of Timed Automata Using Forcible Events
• Discrete-event dynamic systems
• Incorporating Monitors in Reactive Synthesis without Paying the Price
• Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion