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.
Cite
@article{arxiv.2007.01773,
title = {Supervisory Controller Synthesis for Non-terminating Processes is an Obliging Game},
author = {Rupak Majumdar and Anne-Kathrin Schmuck},
journal= {arXiv preprint arXiv:2007.01773},
year = {2021}
}