Publication Details
Title: The Supervisor Synthesis Problem for Unrestricted CTL is NP-complete
Author: M. Antoniotti and B. Mishra
Group: ICSI Technical Reports
Date: November 1995
PDF: ftp://ftp.icsi.berkeley.edu/pub/techreports/1995/tr-95-062.pdf
Overview:
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. Keywords: Discrete Event Systems, Temporal Logic, Supervisor Synthesis
Bibliographic Information:
ICSI Technical Report TR-95-062
Bibliographic Reference:
M. Antoniotti and B. Mishra. The Supervisor Synthesis Problem for Unrestricted CTL is NP-complete. ICSI Technical Report TR-95-062, November 1995
Author: M. Antoniotti and B. Mishra
Group: ICSI Technical Reports
Date: November 1995
PDF: ftp://ftp.icsi.berkeley.edu/pub/techreports/1995/tr-95-062.pdf
Overview:
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. Keywords: Discrete Event Systems, Temporal Logic, Supervisor Synthesis
Bibliographic Information:
ICSI Technical Report TR-95-062
Bibliographic Reference:
M. Antoniotti and B. Mishra. The Supervisor Synthesis Problem for Unrestricted CTL is NP-complete. ICSI Technical Report TR-95-062, November 1995