The Supervisor Synthesis Problem for Unrestricted CTL is NP-complete
Marco Antoniotti, Binay Mishra · 1995
The problem of restricting a finite state model (a Kripke structure) in order to satisfy a set of unrestricted CTL formulae is named the "Unrestricted CTL Supervisor Synthesis Problem" . The finite state model has the characteristics described in [RW87b], that is, its transitions are partitioned between controllable and uncontrollable ones. The set of CTL formulae represents a specification of the desired behavior of the system, which may be achieved through a control action. This note shows the problem to be NP-complete. 1 Introduction This note contains a proof of the NP-completeness for the Unrestricted CTL Supervisor Synthesis Problem as defined in [Ant95]. The problem is defined in terms of a model of the unrestrained behavior of a discrete system or plant P (typically represented as a Finite State Machine) and a specification S of the desired behavior of the system, given as a set of CTL formulae [Eme90]. The model of the system is given following the conventions established ...