Supervisory Controller Synthesis for Nonterminating Processes Is an Obliging Game

DOI10.1109/TAC.2022.3143108MaRDI QIDQ6137513zbMATH OpenOpenAlexFDO

Authors Rupak Majumdar, Anne-Kathrin Schmuck

Publication date 4 September 2023

Published in IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2007.01773

Mathematics Subject Classification ID

Systems theory; control (93-XX)

Abstract: We present a new algorithm to solve the supervisory control problem over non-terminating processes modeled as $omega$-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 $omega$-regular reactive synthesis. Therefore, our reduction results in a symbolic algorithm based on manipulating sets of states using tools from reactive synthesis.

Cited in

(4)

• Synthesizing permissive winning strategy templates for parity games
• Symbolic solution of Emerson-Lei games for reactive synthesis
• Faster and smaller solutions of obliging games
• Contract-based multi-agent logical controller synthesis under uncertainty

This page was built for publication: Supervisory Controller Synthesis for Nonterminating Processes Is an Obliging Game

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137513)