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, MARCO
Primo
;
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.
Si
paper
Discrete event systems;Contro Systems;Model Checking
English
Workshop on Discrete Event Systems
0-85296-664-4
http://www.diee.unica.it/giua/WODES/WODES96/
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.
Antoniotti, M; Mishra, M
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/151956
Citazioni
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
Social impact