On the convexity of right-closed sets and its application to liveness enforcement in Petri Nets

Right-closed set;convexity;integer convexity;polyhedral theory;Petri Nets;Liveness

Salimi, Ehsan

关键词: Right-closed set;    convexity;    integer convexity;    polyhedral theory;    Petri Nets;    Liveness;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/88056/SALIMI-DISSERTATION-2015.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

A set of n-dimensional integral vectors,Nn, is said to be right-closed if for any x 2 , anyvector y x also belongs to it. An integral-setNn is convex if and only if there is a convex setC Rn such that= Int(C), where Int( ) denotes the integral points in the set argument. In thisdissertation, we show that the problem of verifying convexity of a right-closed set is decidable. Followingthis, we present a polynomial time, LP-based algorithm, for verifying the convexity of a right-closedset of integral vectors, when the dimension n isxed. This result is to be viewed against the backdropof the fact that checking the convexity of a real-valued, geometric set can only be accomplished in anapproximate sense; and, the fact that most algorithms involving sets of real-valued vectors do not applydirectly to their integral counterparts. Also, we discuss a grid-search based algorithm for verifying theconvexity of such a set, although not a polynomial time procedure, it is a method that veri es theconvexity of right-closed sets in a reasonable time complexity.On the application side, right-closed sets feature in the synthesis of Liveness Enforcing SupervisoryPolicies (LESPs) for a large family of Petri Nets (PNs). For any PN structure N from this family,the set of initial markings,(N), for which there is a LESP, is right-closed. A LESP determines thetransitions of a PN that are to be permitted tore at any marking in such a manner that, irrespectiveof the past, every transition can bered at some marking in the future. A system that is modeled by alive PN does not experience livelocks, which serves as the motivation for investigating implementationparadigms for LESPs in practice.If a transition is prevented fromring at a marking by a LESP, and all LESPs, irrespective ofthe implementation-paradigm that is chosen, prescribe the same control for the marking, then it is aminimally restrictive LESP. It is possible to synthesize the minimally restrictive LESP for any instance N of the aforementioned family that uses the right-closed set of markings(N). The literature alsocontains an implementation paradigm called invariant-based monitors for liveness enforcement in PNs.This paradigm is popular due to the fact that the resulting supervisor can be directly incorporatedinto the semantics of the PN model of the controlled system. In this work, we show that there is aninvariant-based monitor that is equivalent to the minimally restrictive LESP that uses the right-closedset(N) if and only if(N) is convex. This result serves as the motivation behind exploring theconvexity of right-closed sets.