Sequential synthesis of supervisory policies for discrete-event systems modeled by petri nets

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.