Some observations on supervisory policies that enforce liveness in partially controlled Free-Choice Petri nets

Every arc from a place to a transition in a Free-Choice Petri net (FCPN) is either the unique output arc of the place, or, the unique input arc to the transition [M.H.T. Hack, Analysis of production schemata by Petri nets, Master’s thesis, Massachusetts Institute of Technology, February 1972; W. Reisig, Petri Nets, Springer-Verlag, Berlin, 1985; T. Murata, Petri nets: properties, analysis and applications, Proc. IEEE 77 (4) (1989) 541–580]. We consider FCPNs that are not live [J.L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice-Hall, Englewood Cliffs, NJ, 1981; W. Reisig, Petri Nets, Springer-Verlag, Berlin, 1985; T. Murata, Petri nets: properties, analysis and applications, Proc. IEEE 77 (4) (1989) 541–580], and we investigate the existence of supervisory policies that can enforce liveness in partially controlled FCPNs. The external agent, or supervisor, can only prevent the firing of some (i.e. not all) transitions in a partially controlled FCPN.

We first present an observation on supervisory policies that enforce liveness in partially-controlled FCPNs. Using this observation, we solve the supervisory synthesis problem for the family of c hoice-controlled FCPNs, defined in this paper. We then identify a new, sub-class of partially-controlled FCPNs that posses an easily-characterized (and easily-enforced) supervisory policy that enforces liveness.     

An Application of Independent, Increasing, Free-Choice Petri Nets to the Synthesis of Policies that Enforce Liveness in Arbitrary Petri Nets

The class of Independent, Increasing, Free-Choice Petri nets (II-FCPNs) was introduced in (Sreenivas, 1997c), where it is shown that any II-FCPN can be made live via supervision using a readily available policy. In a live Petri net (PN). Petri Net Theory and Modeling of systems. Prentice-Hall, Englewood Cliffs, NJ, Reisig (1985). Petri Nets. Springer, Berlin), it is possible to fire any transition from every reachable marking, although not necessarily immediately. In this paper we identify a class of PNs, where every transition is controllable, that are not necessarily II-FCPNs, that can be made live via supervision using a readily available policy constructed from the policy that enforces liveness in an II-FCPN.     

On the existence of supervisory policies that enforce liveness indiscrete-event dynamic systems modeled by controlled Petri nets

We consider discrete-state plants represented by controlled Petri nets (CtlPNs), where a subset of transitions can be prevented from firing by a supervisor. A transition in a CtlPN can fire at a marking if there are sufficient tokens in its input places and it is permitted to fire by the supervisor. A CtlPN is live if it is possible to fire any transition from every marking that is reachable under supervision. In this paper we derive a necessary and sufficient condition for the existence of a supervisory policy that enforces liveness in CtlPNs. We show this condition cannot be tested for an arbitrary CtlPN. However, for bounded CtlPNs or CtlPNs, where each transition is individually controllable, we show the existence of a supervisory policy which enforces that liveness is decidable. We also show the existence of a supervisory policy that enforces liveness is necessary and sufficient for the existence of a minimally restrictive supervisory policy     

On supervisory policies that enforce liveness in completelycontrolled Petri nets with directed cut-places and cut-transitions

The process of synthesizing a supervisory policy that enforces liveness in a Petri net (PN), where each transition can be prevented from firing by an external agent, can be computationally burdensome in general. We consider PNs that have a directed cut place or a cut-transition. A place (transition) in a connected PN is said to be a cut place (cut-transition) if its removal will result in two disconnected component PNs. A cut place is said to be a directed cut-place, if in the original PN, all arcs into this cut place emanate from transitions in only one of the two disconnected component PNs. The authors show there is a supervisory policy that enforces liveness in the original PN if and only if similar policies exist for two PNs derived from the disconnected components obtained after the removal of the directed cut-place (cut-transition). The utility of this observation in alleviating the computational burden of policy synthesis is illustrated via example     

Liveness-enforcing supervision of bounded ordinary Petri nets usingpartial order methods

This paper combines and refines recent results into a systematic way to verify and enforce the liveness of bounded ordinary Petri nets. The approach we propose is based on a partial-order method called network unfolding. Network unfolding maps the original Petri net to an acyclic occurrence net. A finite prefix of the occurrence net is defined to give a compact representation of the original net reachability graph while preserving the causality between net transitions. A set of transition invariants denoted as base configurations is identified in the finite prefix. These base configurations capture all of the fundamental executions of the net system, thereby providing a modular way to verify and synthesize supervisory net systems. This paper proves necessary and sufficient conditions that characterize the original net liveness and the existence of maximally permissive supervisory policies that enforce liveness     

On Supervisory Policies that Enforce Global Fairness and Bounded Fairness in Partially Controlled Petri Nets

In this paper we consider the notions of global-fairness (G-fairness) and bounded-fairness (B-fairness) for arbitrary Petri nets (PNs). G-fairness in a PN guarantees every transition occurs infinitely often in every valid firing sequence of infinite length. B-fairness guarantees a bound on the number of times a transition in the PN can fire without some transition firing at least once. These properties are guaranteed without recourse to assumptions on firing time distributions or contention resolution policies. We present a necessary and sufficient condition for the existence of supervisory policies that enforce G-fairness and B-fairness along with various observations on the closure properties of policies that enforce these notions of fairness in controlled PNs with a (possibly) non-empty set of uncontrollable transitions. We also derive a necessary and sufficient condition that guarantees a minimally restrictive supervisor that enforces these notions of fairness for bounded PNs. These results are illustrated via examples.     

Necessary and sufficient liveness condition of GS3PR Petri nets

Structural analysis is one of the most important and efficient methods to investigate the behaviour of Petri nets. Liveness is a significant behavioural property of Petri nets. Siphons, as structural objects of a Petri net, are closely related to its liveness. Many deadlock control policies for flexible manufacturing systems (FMS) modelled by Petri nets are implemented via siphon control. Most of the existing methods design liveness-enforcing supervisors by adding control places for siphons based on their controllability conditions. To compute a liveness-enforcing supervisor with as much as permissive behaviour, it is both theoretically and practically significant to find an exact controllability condition for siphons. However, the existing conditions, max, max′, and max″-controllability of siphons are all overly restrictive and generally sufficient only. This paper develops a new condition called max*-controllability of the siphons in generalised systems of simple sequential processes with resources (GS³PR), which are a net subclass that can model many real-world automated manufacturing systems. We show that a GS³PR is live if all its strict minimal siphons (SMS) are max*-controlled. Compared with the existing conditions, i.e., max-, max′-, and max″-controllability of siphons, max*-controllability of the SMS is not only sufficient but also necessary. An example is used to illustrate the proposed method.     

Design of T-liveness enforcing supervisors in Petri nets

This paper presents a procedure for the design of supervisors that enforce the transitions in a given set T to be live. T-liveness enforcement corresponds to full liveness enforcement when T equals the total set of transitions. Rather than assuming a given initial marking, this procedure generates at every iteration a convex set of admissible initial markings. In the case of full liveness enforcement and under certain conditions also in the case of T-liveness enforcement, the convex set of each iteration includes the set of markings for which liveness/T-liveness can be enforced. When the procedure terminates, and if it terminates, the final convex set contains only markings for which T-liveness can be enforced. Then, the supervisor keeping the Petri net (PN) marking in this convex set can be easily designed using the place invariant based approach. This paper focuses on the fully controllable and observable PNs. Several extensions of the procedure, including to partially controllable and observable PNs, are outlined.     

On computing the supremal right-closed control invariant subset of a right-closed set of markings for an arbitrary petri net

A set of non-negative integral vectors is said to be right-closed if the presence of a vector in the set implies all term-wise larger vectors also belong to the set. A set of markings is control invariant with respect to a Petri Net (PN) structure if the firing of any uncontrollable transition at any marking in this set results in a new marking that is also in the set. Every right-closed set of markings has a unique supremal control invariant subset, which is the largest subset that is control invariant with respect to the PN structure. This subset is not necessarily right-closed. In this paper, we present an algorithm that computes the supremal right-closed control invariant subset of a right-closed of markings with respect to an arbitrary PN structure. This set plays a critical role in the synthesis of Liveness Enforcing Supervisory Policies (LESPs) for a class of PN structures, and consequently, the proposed algorithm plays a key role in the synthesis of LESPs for this class of PN structures.

     

Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols

State-based formal methods [e.g. Event-B/RODIN (Abrial in Modeling in Event-B—system and software engineering. Cambridge University Press, Cambridge, 2010; Abrial et al. in Int J Softw Tools Technol Transf (STTT) 12(6):447–466, 2010)] for critical system development and verification are now well established, with track records including tool support and industrial applications. The focus of proof-based verification, in particular, is on safety properties. Liveness properties, which guarantee eventual, or converging computations of some requirements, are less well dealt with. Inductive reasoning about liveness is not explicitly supported. Liveness proofs are often complex and expensive, requiring high-skill levels on the part of the verification engineer. Fairness-based temporal logic approaches have been proposed to address this, e.g. TLA Lamport (ACM Trans Program Lang Syst 16(3):872–923, 1994) and that of Manna and Pnueli (Temporal verification of reactive systems—safety. Springer, New York, 1995). We contribute to this technology need by proposing a fairness-based method integrating temporal and first-order logic, proof and tools for modelling and verification of safety and liveness properties. The method is based on an integration of Event-B and TLA. Building on our previous work (Méry and Poppleton in Integrated formal methods, 10th international conference, IFM 2013, Turku, Finland, pp 208–222, 2013. doi: 10.1007/978-3-642-38613-8_15), we present the method via three example population protocols Angluin et al. (Distrib Comput 18(4):235–253, 2006). These were proposed as a theoretical framework for computability reasoning about Wireless Sensor Network and Mobile Ad-Hoc Network algorithms. Our examples present typical liveness and convergence requirements. We prove convergence results for the examples by integrated modelling and proof with Event-B/RODIN and TLA. We exploit existing proof rules, define and apply three new proof rules; soundness proofs are also provided. During the process we observe certain repeating patterns in the proofs. These are easily identified and reused because of the explicit nature of the reasoning.     

Minimizing Place Capacities of Weighted Event Graphs for Enforcing Liveness

This paper addresses the problem of minimizing place capacities of weighted event graphs in order to enforce liveness. Necessary and sufficient conditions of the solution existence are derived. Lower bounds of place capacities while preserving liveness are established and a polynomial algorithm is proposed to determine an initial marking leading to these lower bounds while preserving the liveness.

Centralized and decentralized supervisory controller design to enforce boundedness,liveness, and reversibility in Petri nets

Supervisory controller design to enforce boundedness, liveness, and reversibility in Petri nets is considered. The Petri nets considered may have non-unity weight arcs and both controllable and uncontrollable transitions. Algorithms for a centralized controller design approach are first developed. The developed algorithms always find a controller whenever it exists. This controller enforces boundedness, liveness, and reversibility; it also avoids deadlock. Furthermore, it is shown that the controller obtained is the least restrictive controller among all controllers which enforce desired properties. A decentralized controller design approach, based on overlapping decompositions, is then introduced. Algorithms to design decentralized controllers based on this approach are also developed. These controllers, when they exist, also guarantees boundedness, liveness, reversibility and deadlock freeness. The decentralized controllers have two main advantages over the centralized ones. First, they have reduced on-line computation and communication requirements. Second, the computational time required to design decentralized controllers is considerably less than that required for centralized controllers.     

From liveness to promptness

Liveness temporal properties state that something “good” eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the “wait time” for an eventuality to be fulfilled. That is, F θ asserts that θ holds eventually, but there is no bound on the time when θ will hold. This is troubling, as designers tend to interpret an eventuality F θ as an abstraction of a bounded eventuality F ^≤k θ, for an unknown k, and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here prompt-LTL, an extension of LTL with the prompt-eventually operator F _p . A system S satisfies a prompt-LTL formula φ if there is some bound k on the wait time for all prompt-eventually subformulas of φ in all computations of S. We study various problems related to prompt-LTL, including realizability, model checking, and assume-guarantee model checking, and show that they can be solved by techniques that are quite close to the standard techniques for LTL.     

时间Petri网保持活性、有界性的两个充要条件

活性和有界性是Petri网最重要的性质，对于传统Petri网的这些性质，国内外学者作过大量的研究工作，并且得到了不少成果，而对含时间因素的Petri网的这些相应性质国内外研究得很少。本文首先介绍了时间Petri网TPN的若干基本定义，然后说明了时间Petri网TPN的活性、有界性和对应传统Petri网的相应性质并无关系，接着给出了时间Petri网保持活性、有界性的时间区间上的两个充分强要条件。为利用传统Petri网的性质判定结果来判定时间Petri网的相应性质提供了可能性。     

Design of Optimal Petri Net Supervisors for Flexible Manufacturing Systems via Weighted Inhibitor Arcs

This paper develops an approach to the design of an optimal Petri net supervisor that enforces liveness to flexible manufacturing systems. The supervisor contains a set of observer places with weighted inhibitor arcs. An observer place with a weighted inhibitor arc is used to forbid a net from yielding an illegal marking by inhibiting the firing of a transition at a marking while ensuring that all legal markings are preserved. A marking reduction technique is presented to decrease the number of considered markings, which can dramatically lower the computational burden of the proposed approach. An integer linear program is presented to simplify the supervisory structure by minimizing the number of observer places. Finally, several examples are used to shed light on the proposed approach which can lead to an optimal supervisor for the net models that cannot be optimally controlled via pure Petri net supervisors.     

Integrating a wavelet based perspiration liveness check with fingerprint recognition

It has been shown that fingerprint scanners can be deceived very easily, using simple, inexpensive techniques. In this work, a countermeasure against such attacks is enhanced, that utilizes a wavelet based approach to detect liveness, integrated with the fingerprint matcher. Liveness is determined from perspiration changes along the fingerprint ridges, observed only in live people. The proposed algorithm was applied to a data set of approximately 58 live, 50 spoof and 28 cadaver fingerprint images captured at 0 and 2 s, from each of three different types of scanners, for normal conditions. The results demonstrate perfect separation of live and not live for the normal conditions. Without liveness module the commercially available verifinger matcher is shown to give equal error rate (EER) of 13.85% where false reject rate is calculated for genuine-live users and false accept rate is for genuine-not live, imposter-live and imposter-not live. The integrated system of fingerprint matcher and liveness module reduces EER to 0.03%. Results are also presented for moist and dry fingers simulated by glycerin and acetone, respectively. The system is further tested using gummy fingers and various deliberately simulated conditions including pressure change and adding moisture to the spoof to analyze the strength of the liveness algorithm.     

Synthesis of liveness enforcing supervisor for automated manufacturing systems using insufficiently marked siphons

A liveness enforcing supervisor synthesis technique is presented for Petri net modeling automated manufacturing systems. The insufficiently marked siphons are deployed to characterize the deadlock situations in an incidence matrix based way, which makes possible the study of the modeled systems from both structural and algebraic perspectives. The approach generates at each step a generalized mutual exclusion constraint which contains only markings for which liveness can be enforced. To avoid the explicit enumeration of all the set of strict minimal siphons, a set of mathematical programming formulations are established to implement the derivation of insufficiently marked siphons from the PT-transformation of the plant system. Further, a generalized elementary siphon control approach is involved such that the final supervisor can be structurally simplified. Several examples are used to illustrate these results.     

Closed-loop Live Marked Graphs under Generalized Mutual Exclusion Constraint Enforcement

Enforcing a supervisory control policy to avoid forbidden states on a discrete event system modeled by a Petri net may result in a non live system. This may happen even if the admissible states are specified by Generalized Mutual Exclusion Constraints (GMECs). This leads to the problem of synthesizing a maximally permissive control policy preserving liveness of the system under a GMEC. This problem is very interesting in practice, but difficult even for a restricted class of systems. In this paper, we focus on systems which can be modeled as live and safe Marked Graphs (MGs). On such systems, when some of the transitions are uncontrollable, a GMEC can be forced by a monitor place if a not maximally permissive policy is accepted, otherwise a more complex control has to be adopted. Anyway, liveness of the closed-loop system (plant plus control) is not guaranteed. Two sufficient conditions to verify the closed-loop liveness of a live and safe MG plant controlled by a monitor are derived. A sufficient condition for closed loop liveness of MGs where a GMEC has been enforced on is derived. In addition, a set of predicates is provided that enforces, in a maximally permissive way, a GMEC while preserving closed-loop liveness on live and safe MG systems under some restrictions.

Notes on Liveness and Boundedness of Extended Strong Asymmetric Choice Nets Ⅱ

In this paper,the Extended Strong,Asymmetric Choice NetsⅡ（ESACNⅡ),a subclass of Asymmetric Choice Nets(ACN) including Extended Free Choice Nets(EFCN) and Strong Asymmetric Choice Nets Ⅱ(SACNⅡ),is presented.A necessary and sufficient condition for liveress of ESACNⅡis proposed.Moreover,a criterion is introduced,which is necessary and sufficient for judgement of liveness and boundedness of ESACNⅡ,Meanwhile a polynomial time algoirithm is given to decide liveness and boundedness for ESACNⅡ.     

Integrated design of optimal supervisors for the enforcement of static and behavioral specifications in Petri net models

Petri net (PN) supervisory control is often performed through a sequential procedure that introduces additional constraint layers over an initial unconstrained PN model, using generalized mutual exclusion constraints (GMECs) implemented as monitor places. This is typical, e.g., in the context of flexible manufacturing systems, where the initial model represents the production sequences and the constraints are used to express static specifications, such as job limitations or the usage of resources, and behavioral ones, as liveness, controllability, etc. This sequential procedure may yield a redundant model, that is not easily reduced a posteriori. Also, it is difficult to ensure maximal permissivity with respect to multiple behavioral specifications. This paper, building on recent results regarding optimal supervisor design with branch & bound methods, proposes an integrated modeling approach that can be used to derive a minimal supervisor guaranteeing the attainment of an arbitrary set of static and behavioral specifications in a maximally permissive way. Among behavioral specifications, deadlock-freeness, liveness, reversibility and behavioral controllability are considered in the paper. The supervisor comes in the form of a simple set of GMECs or of a disjunction of sets of GMECs. Some examples emphasize the potential model size reductions that can be achieved.