On commoner's liveness theorem and supervisory policies that enforce liveness in free-choice Petri nets

A Petri net (PN) (Peterson, 1981; Reisig, 1985) is said to be live if it is possible to fire any transition from every reachable marking, although not necessarily immediately. A free-choice Petri net FCPN) is a PN, where every arch from a place to a transition is either the unique output arc from that place or it is the unique input arc to the transition. Commoner's Liveness Theorem (cf. Hack, 1972, Ch. 4; Reisig, 1985, Section 7.2) states that a FCPN is live if and only if every siphon contains a marked trap at the initial marking. A siphon (trap) is a collection of places P such that . We concern ourselves with marking-dependent supervisory policies that can prevent the firing of a transition. We characterize supervisory policies that enforce liveness in non-live FCPNs using observations that strongly parallel Commoner's Liveness Theorem. We use this characterization to establish the existence of supervisory policies that enforce liveness in a Class of FCPNs called independent, increasing free-choice petri nets (II-FCPNs).     

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.     

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     

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.     

Reduction of the supervisory control problem for Petri nets

The authors prove a reduction theorem for the supervisory control problem for general Petri nets with general legal sets. To design control laws guaranteeing that the marking stays within the legal set, it suffices to consider a sub-Petri net of the full model. This extends existing design algorithms, allows to prove an important property of maximally permissive control laws and limits the number of events which need to be observed     

Blocking and controllability of Petri nets in supervisory control

This note discusses the use of Petri net languages in supervisory control theory. First it is shown that the trimming of an unbounded Petri net is not always possible and a new class of Petri net languages, that may be generated by nonblocking nets, is defined. Secondly, necessary and sufficient conditions for the existence of a Petri net supervisor, under the hypothesis that the system's behavior and the legal behavior are both Petri net languages, are derived. Finally, by means of an example, it is shown that Petri net languages are not closed under the supremal controllable sublanguage operator     

Model checking Petri nets with names using data-centric dynamic systems

Petri nets with name creation and management (\({\nu}\)-PNs) have been recently introduced as an expressive model for dynamic (distributed) systems, whose dynamics are determined not only by how tokens flow in the system, but also by the pure names they carry. On the one hand, this extension makes the resulting nets strictly more expressive than P/T nets: they can be exploited to capture a plethora of interesting systems, such as distributed systems enriched with channels and name passing, service interaction with correlation mechanisms, and resource-constrained workflow nets that explicitly account for process instances. On the other hand, fundamental properties like coverability, termination and boundedness are decidable for \({\nu}\)-PNs. In this work, we go one step beyond the verification of such general properties, and provide decidability and undecidability results of model checking \({\nu}\)-PNs against variants of first-order \({\mu}\)-calculus, recently proposed in the area of data-aware process analysis. While this model checking problem is undecidable in the general case, decidability can be obtained by considering different forms of boundedness, which still give raise to an infinite-state transition system. We then ground our framework to tackle the problem of soundness checking over workflow nets enriched with explicit process instances and resources. Notably, our decidability results are obtained via a translation to data-centric dynamic systems, a recently devised framework for the formal specification and verification of data-aware business processes working over full-fledged relational databases with constraints. In this light, our results contribute to the cross-fertilization between the area of formal methods for concurrent systems and that of foundations of data-aware processes, which has not been extensively investigated so far.     

On conditions for the liveness of weakly persistent nets

This paper first proves that each minimal siphon in a weakly persistent net is a trap if its pre-set is nonempty. Therefore, each minimal siphon contains a marked trap if a weakly persistent net is live for an initial marking. Next, it is proved that the condition, each minimal siphon contains a marked trap, is both necessary and sufficient for the liveness of weakly persistent nets if these nets additionally satisfy the asymmetric choice property or the intrinsic fairness.     

A parameterized liveness and ratio-enforcing supervisor for a class of generalized Petri nets

The work proposes a synthesis method of supervisors for flexible manufacturing systems modeled by a class of generalized Petri nets. A concept of resource usage ratios (RU-ratios) is first presented to describe the occupation degree of a resource by an operation. Next, an intrinsically live structure characterized by a special numerical relationship between arc-weights and initial markings is investigated from a perspective of RU-ratios. Then, a new kind of supervisors is synthesized on the ground of the generic nature of the intrinsically live structure. Such a supervisor can achieve the purposes of both liveness-enforcement and resource usage ratio-enforcement of the system under consideration. Given a plant, it is easy to determine the topological structure of such a supervisor and the number of monitors is bounded by that of resources used in the plant. In addition, when the configuration of the plant model changes, the supervisor can be reusable through adjusting control parameters only without rearrangement of connections. This makes it easy enough and intuitive to be used by industrial practitioners. Instead of maximal behavioral permissiveness, it pursues a precise usage of shared resources that are limited and valuable. Several examples are used to illustrate the proposed methods.     

On forbidden state problems for a class of controlled Petri nets

This paper treats the forbidden state problem for the class of discrete-event dynamical systems (DEDS's) which can be modeled as controlled state machines (CtlSM's). CtlSM's constitute a special class of controlled Petri nets (CtlPN's) where no synchronization requirements are included in the system model. Synchronization and other safety requirements are modeled via sets of forbidden states. In this paper we study methods guaranteeing these constraints by disabling some of the controllable transitions. We assume that the full state is observable. Control logic synthesis taking into account the graphical representation of CtlSM's and the distributed state representation in terms of markings is proposed and justified. Two examples-the cat-and-mouse game and a model of a metro line-illustrate the theoretical results     

On optimal supervisory control with trimness of controlled systems

In this paper, we propose a design algorithm for an optimal supervisor for guaranteeing the trimness of the controlled system. We generalize the earlier work of Kumar and Grag based on the induced flow network of a given discrete event system. Specifically, the proposed algorithm is directly applicable to a discrete event system and minimizes the net cost of the optimal supervisor, which ensures that the controlled system is a trim generator with a polynomial-order computational complexity.     

On reachability graphs of Petri nets

Petri net is a powerful tool for system analysis and design. Several techniques have been developed for the analysis of Petri nets, such as reachability trees, matrix equations and reachability graphs. This article presents a novel approach to constructing a reachability graph, and discusses the application of the reachability graph to Petri nets analysis.     

Identification of the unobservable behaviour of industrial automation systems by Petri nets

This paper addresses the problem of identifying the model of the unobservable behaviour of discrete event systems in the industrial automation sector. Assuming that the fault-free system structure and dynamics are known, the paper proposes an algorithm that monitors the system on-line, storing the occurred observable event sequence and the corresponding reached states. At each event observation, the algorithm checks whether some unobservable events have occurred on the basis of the knowledge of the Petri net (PN) modelling the nominal system behaviour and the knowledge of the current PN marking. By defining and solving some integer linear programming problems, the algorithm decides whether it is necessary to introduce some unobservable (silent) transitions in the PN model and provides a PN structure that is consistent with the observed event string. A case study describing an industrial automation system shows the efficiency and the applicability of the proposed algorithm.     

Symbolic execution of concurrent systems using Petri nets

Techniques for analyzing sequential programs in order to improve their reliability have been widely studied in the past. Among the most interesting analysis techniques, we consider symbolic execution. However, analysis techniques for concurrent programs, and in particular symbolic execution, are still an open research area. In this paper, we define a method for symbolic execution of concurrent systems, based on an extension of the Petri net formalism, called EF nets. EF nets are a powerful, highly expressive and general formalism. Depending on the level of abstraction of actions and predicates that one associates to the transitions of the net, EF nets can be used as a high-level specification formalism for concurrent systems, or as a lower level internal representation of concurrent programs. Thus, the model is not dependent on a particular concurrent programming language, but it is flexible enough to be the kernel model for the representation of a wide set of systems and programming languages. In the paper, in order to support the analysis of a concurrent system or program, at first a general algorithm for symbolically executing an EF net is defined. Then, a more efficient algorithm is given for the particular, though important, subclass of EF nets, defined as safe EF nets. Such algorithm is proved to significantly help in reducing the amount of information needed to characterize a symbolic execution. Both the modelling power of the EF nets and the usefulness of the concurrent symbolic execution algorithms defined are illustrated by means of a case study.     

Performance evaluation of parallel systems by using unboundedgeneralized stochastic Petri nets

Methods of calculating efficiently the performance measures of parallel systems by using unbounded generalized stochastic Petri nets are presented. An explosion in the number of states to be analyzed occurs when unbounded places appear in the model. The state space of such nets is infinite, but it is possible to take advantage of the natural symmetries of the system to aggregate the states of the net and construct a finite graph of lumped states which can easily be analyzed. With the methods developed, the unbounded places introduce a complexity similar to that of safe places of the net. These methods can be used to evaluate models of open parallel systems in which unbounded places appear; systems which are k-bounded but are complex and have large values of k can also be evaluated in an appropriate way. From the steady-state solution of the model, it is possible to obtain automatically the performance measures of parallel systems represented by this type of net     

Suboptimal supervisory control of Petri nets in presence of uncontrollable transitions via monitor places

This paper deals with the problem of enforcing generalized mutual exclusion constraints (GMEC) on place/transition nets with uncontrollable transitions. An efficient control synthesis technique, which has been proposed in the literature, enforces GMEC constraints by introducing monitor places to create suitable place invariants. The method has been shown to be maximally permissive and to give a unique control structure in the case that the set of legal markings is controllable. This paper investigates on and formally shows that the class of controllers obtained by this technique may not have a supremal element for uncontrollable specifications. Moreover, it is shown that the family of monitor places enforcing an uncontrollable specification can be parameterized with respect to the solution of a linear system of equation. An algorithm to obtain such parameterization is presented here.     

The effect of execution policies on the semantics and analysis ofstochastic Petri nets

Petri nets in which random delays are associated with atomic transitions are defined in a comprehensive framework that contains most of the models already proposed in the literature. To include generally distributed firing times into the model one must specify the way in which the next transition to fire is chosen, and how the model keeps track of its past history; this set of specifications is called an execution policy. A discussion is presented of the impact that different execution policies have on semantics of the mode, as well as the characteristics of the stochastic process associated with each of these policies. When the execution policy is completely specified by the transition with the minimum delay (race policy) and the firing distributions are of the phase type, an algorithm is provided that automatically converts the stochastic process into a continuous time homogeneous Markov chain. An execution policy based on the choice of the next transition to fire independently of the associated delay (preselection policy) is introduced, and its semantics is discussed together with possible implementation strategies