Petri net controller synthesis using theory of regions
Petri net controller synthesis is formally treated in this paper. Two supervisory control problems of plant Petri net models, forbidden state problem and forbidden state-transition problem, are defined. The theory of regions is used to provide algebraic characterizations of pure control places and impure control places for both problems. Thanks to Farkas-Minkowski's lemma, the algebraic characterizations lead to nice geometric characterization for the existence of control places for the two supervisory problems. A railway network application is presented.
Excellent work!!
Is there a formal guarantee that the generated PN is valid and sound? Could you please explain in detail how the following is guarantied? 1. For any case, it is possible to terminate, i.e., it is possible to reach a state with at least one token in the output place o
2. There are no dangling references, i.e., the moment the case terminates (i.e., a token appears in o), there are no tokens left behind
This paper proposes a rigorous technique designing PN controllers. What are the advantages of the proposed technique compared with others? What other applications has the theory of regions been put to?