摘要：AbstractThis 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 overfinitewords. In particular, we show that the deterministic finite automatonGtypically used in SCT to construct amaximally permissive supervisor ffor a plant languageLw.r.t. a specification languageE, 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 overG. 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.
关键词：KeywordsDiscrete-event systemssupervisory controlreactive synthesisµ-calculusgame theory
