TY - GEN
T1 - Sequential synthesis of supervisory policies for discrete-event systems modeled by petri nets
AU - Raman, A.
AU - Sreenivas, R. S.
N1 - Funding Information:
This work was supported in part by the Arthur Davis Faculty Scholar Endowment at the University of Illinois at Urbana-Champaign.
Publisher Copyright:
© 2019 IEEE.
PY - 2019/10
Y1 - 2019/10
N2 - It is often of interest to synthesize a supervisory policy for enforcing complex properties on the behaviour of a Discrete-Event System (DES). One way of doing this is by decomposing complex properties into simpler objectives and then synthesizing supervisors for those simpler objectives in a sequential manner. This approach is particularly convenient if the supervised-system can be represented using the same modeling framework at each stage of this sequential process. An additional desirable feature could be that the supervisory policy remain the same even if the initial-state of the DES were to change. In this paper, we consider Petri Net (PN) models of Discrete-Event Systems (DES) under a supervisory policy that enforces a desired-property B. We prove that the supervised-system can be modeled as a PN if and only if the supervisory policy is a marking-monotone-B-enforcing supervisory policy (MM-BESP) over reachable markings. In the second half of the paper we describe a software tool for the synthesis of MM-BESPs, where the desired-property B is the PN-property of liveness, for arbitrary Petri Nets. We end the paper with an example that illustrates both the contributions.
AB - It is often of interest to synthesize a supervisory policy for enforcing complex properties on the behaviour of a Discrete-Event System (DES). One way of doing this is by decomposing complex properties into simpler objectives and then synthesizing supervisors for those simpler objectives in a sequential manner. This approach is particularly convenient if the supervised-system can be represented using the same modeling framework at each stage of this sequential process. An additional desirable feature could be that the supervisory policy remain the same even if the initial-state of the DES were to change. In this paper, we consider Petri Net (PN) models of Discrete-Event Systems (DES) under a supervisory policy that enforces a desired-property B. We prove that the supervised-system can be modeled as a PN if and only if the supervisory policy is a marking-monotone-B-enforcing supervisory policy (MM-BESP) over reachable markings. In the second half of the paper we describe a software tool for the synthesis of MM-BESPs, where the desired-property B is the PN-property of liveness, for arbitrary Petri Nets. We end the paper with an example that illustrates both the contributions.
UR - http://www.scopus.com/inward/record.url?scp=85076720390&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85076720390&partnerID=8YFLogxK
U2 - 10.1109/SMC.2019.8914207
DO - 10.1109/SMC.2019.8914207
M3 - Conference contribution
AN - SCOPUS:85076720390
T3 - Conference Proceedings - IEEE International Conference on Systems, Man and Cybernetics
SP - 2372
EP - 2377
BT - 2019 IEEE International Conference on Systems, Man and Cybernetics, SMC 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2019 IEEE International Conference on Systems, Man and Cybernetics, SMC 2019
Y2 - 6 October 2019 through 9 October 2019
ER -