A μ-calculus approach for the synthesis of discrete-event supervisors with safety specifications

In this paper we present a generalized model-checking-based approach for the synthesis of automata-based supervisors for discrete-event systems (DES). Expressiveness of μ-calculus is exploited to construct fixpoint operators for supervisory synthesis. A novel Kripke structure is proposed that simplifies the synthesis of supervisors as a model checking problem within the same approach. An efficient synthesis algorithm is presented maintaining the same computational complexity of other known methods. A graphical example is employed to show the advantages of the proposed approach.