The problem of restricting a nite state mo del a Kripke structure in order to satisfy a set of unrestricted CTL formul is named the Unrestricted CTL Supervisor Synthesis Problem. The finite state model has the characteristics describ ed in Ramadge and Wonham, 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.
Antoniotti, M., Mishra, M. (1996). NP-completeness of the Supervisor Synthesis Problem for Unrestricted CTL Specifications. In Proceedings of the International Workshop on Discrete Event Systems, WODES 1996.
NP-completeness of the Supervisor Synthesis Problem for Unrestricted CTL Specifications
ANTONIOTTI, MARCOPrimo
;
1996
Abstract
The problem of restricting a nite state mo del a Kripke structure in order to satisfy a set of unrestricted CTL formul is named the Unrestricted CTL Supervisor Synthesis Problem. The finite state model has the characteristics describ ed in Ramadge and Wonham, 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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
