LAUSR

This paper establishes a connection between supervisory control theory (SCT) and reactive synthesis (RS) in the situation where both the plant and the specification are modeled by ∗-languages, i.e., formal languages over finite words. In particular, we show that the deterministic finite automaton G typically used in SCT to construct a maximally permissive supervisor f for a plant language L w.r.t. a specification language E, can be interpreted as a two-player game which allows to solve the considered synthesis problem by a two-nested fixed-point algorithm in the μ-calculus over G. The resulting game turns out to be a cooperative Büchi-type game which allows for a maximally permissive solution in the particular context of SCT. This is surprising, as classical Büchi games do not have this property.