The Supervisor Synthesis Problem for Unrestricted CTL is NP-complete
Title | The Supervisor Synthesis Problem for Unrestricted CTL is NP-complete |
Publication Type | Technical Report |
Year of Publication | 1995 |
Authors | Antoniotti, M., & Mishra B. |
Other Numbers | 1002 |
Keywords | Discrete Event Systems, Supervisor Synthesis, Temporal Logic |
Abstract | The problem of restricting a finite state model (a Kripke structure) in order to satisfy a set of unrestricted CTL formulas is named the "Unrestricted CTL Supervisor Synthesis Problem." The finite state model has the characteristics described by Ramadge and Wonham, that is, its transitions are partitioned between controllable and uncontrollable ones. The set of CTL formulas 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. |
URL | http://www.icsi.berkeley.edu/ftp/global/pub/techreports/1995/tr-95-062.pdf |
Bibliographic Notes | ICSI Technical Report TR-95-062 |
Abbreviated Authors | M. Antoniotti and B. Mishra |
ICSI Publication Type | Technical Report |