The Supervisor Synthesis Problem for Unrestricted CTL is NP-complete

TitleThe Supervisor Synthesis Problem for Unrestricted CTL is NP-complete
Publication TypeTechnical Report
Year of Publication1995
AuthorsAntoniotti, M., & Mishra B.
Other Numbers1002
KeywordsDiscrete 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.

URLhttp://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