Using Model Checking to Solve Supervisor Synthesis Problems

Verification procedures, which check whether a given system satisfies a given specification, are nowadays mature for industrial usage. The more general supervisor synthesis problem asks how a system has to be restricted or which actions have to be selected such that the system satisfies a given specification. Supervisor synthesis problems are often formulated in frameworks like game structures that are more general than the Kripke structures that are traditionally used in verification. For this reason, current verification tools can not be used for supervisory control problems. In this paper, however, we present a reduction of alternating time μ-calculus model checking problems (on game structures) to model checking problems of the μ-calculus on Kripke structures. As a result, arbitrary model checkers can be used to solve supervisor synthesis problems. As a demonstration of the applicability of our approach, we show how the classical supervisory control problems of Ramadge and Wonham can be solved within our framework.