Files in this item



application/pdfSALIMI-DISSERTATION-2015.pdf (1MB)
(no description provided)PDF


Title:On the convexity of right-closed sets and its application to liveness enforcement in Petri Nets
Author(s):Salimi, Ehsan
Director of Research:Sreenivas, Ramavarapu S.
Doctoral Committee Chair(s):Sreenivas, Ramavarapu S.
Doctoral Committee Member(s):Basar, Tamer; Nagi, Rakesh; Beck, Carolyn L.; Kiyavash, Negar
Department / Program:Industrial&Enterprise Sys Eng
Discipline:Industrial Engineering
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Right-closed set
integer convexity
polyhedral theory
Petri Nets
Abstract:A set of n-dimensional integral vectors, Nn, is said to be right-closed if for any x 2 , any vector y x also belongs to it. An integral-set Nn is convex if and only if there is a convex set C Rn such that = Int(C), where Int( ) denotes the integral points in the set argument. In this dissertation, we show that the problem of verifying convexity of a right-closed set is decidable. Following this, we present a polynomial time, LP-based algorithm, for verifying the convexity of a right-closed set of integral vectors, when the dimension n is xed. This result is to be viewed against the backdrop of the fact that checking the convexity of a real-valued, geometric set can only be accomplished in an approximate sense; and, the fact that most algorithms involving sets of real-valued vectors do not apply directly to their integral counterparts. Also, we discuss a grid-search based algorithm for verifying the convexity of such a set, although not a polynomial time procedure, it is a method that veri es the convexity of right-closed sets in a reasonable time complexity. On the application side, right-closed sets feature in the synthesis of Liveness Enforcing Supervisory Policies (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 the transitions of a PN that are to be permitted to re at any marking in such a manner that, irrespective of the past, every transition can be red at some marking in the future. A system that is modeled by a live PN does not experience livelocks, which serves as the motivation for investigating implementation paradigms for LESPs in practice. If a transition is prevented from ring at a marking by a LESP, and all LESPs, irrespective of the implementation-paradigm that is chosen, prescribe the same control for the marking, then it is a minimally 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 also contains 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 incorporated into the semantics of the PN model of the controlled system. In this work, we show that there is an invariant-based monitor that is equivalent to the minimally restrictive LESP that uses the right-closed set (N) if and only if (N) is convex. This result serves as the motivation behind exploring the convexity of right-closed sets.
Issue Date:2015-07-16
Rights Information:Copyright 2015 Ehsan Salimi
Date Available in IDEALS:2015-09-29
Date Deposited:August 201

This item appears in the following Collection(s)

Item Statistics