POC net,a subclass of Petri nets,and its application to timed Petri nets

Liveness is one of the most important properties of the Petri net analysis. This property is concerned with a capability for firing of transitions. On the other hand, place-liveness is another notion related to liveness, which is concerned with a capability for having tokens in places. Concerning these liveness and place-liveness problems, this paper suggests a new subclass of Petri net, ‘POC nets’, as a superclass of AC nets and DC nets. For this subclass, the equivalence between liveness and place-liveness is shown and a sufficient condition for liveness for this POC net is derived. Then the results are extended to liveness problem of timed Petri nets which have transitions with finite firing durations and the earliest firing rule. Although liveness of a (non-timed) Petri net is neither necessary nor sufficient condition for liveness of a timed Petri net, it is shown that liveness is preserved if the net has POC structure. Furthermore, it is pointed out that if a POC net satisfies some additional condition, Petri net liveness is equivalent to timed Petri net liveness. Finally, it is shown that liveness of timed POC nets with TC structure and the earliest firing rule is decidable with deterministic polynomial time complexity.     

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.     

Canonical prefixes of Petri net unfoldings

In this paper, we develop a general technique for truncating Petri net unfoldings, parameterized according to the level of information about the original unfolding one wants to preserve. Moreover, we propose a new notion of completeness of a truncated unfolding. A key aspect of our approach is an algorithm-independent notion of cut-off events, used to truncate a Petri net unfolding. Such a notion is based on a cutting context and results in the unique canonical prefix of the unfolding. Canonical prefixes are complete in the new, stronger sense, and we provide necessary and sufficient conditions for its finiteness, as well as upper bounds on its size in certain cases. A surprising result is that after suitable generalization, the standard unfolding algorithm presented in [8], and the parallel unfolding algorithm proposed in [12], despite being non-deterministic, generate the canonical prefix. This gives an alternative correctness proof for the former algorithm, and a new (much simpler) proof for the latter one.Received: 29 April 2003, Published online: 2 September 2003     

Decentralized supervisory controller design to avoid deadlock in Petri nets

A decentralized supervisory controller design approach, using overlapping decompositions, is proposed for discrete-event systems modelled by Petri nets to avoid deadlock. In this approach, the given original Petri net is first decomposed into overlapping Petri subnets. A controller for each disjoint Petri subnet is then designed. A controller for the expanded Petri net is next obtained by combining these controllers in a certain way. In the final phase, the controller obtained for the expanded Petri net is contracted in a certain way to obtain a controller for the original Petri net. It is proved that this final controller avoids deadlock in the original Petri net.     

Petri网展开图法的分析和应用

Petri网的展开图是一种特殊的并发系统状态空间搜索方法，它不需要重复考虑并发事件的所有可能的交集，从而大大缩减状态空间爆炸给验证分析带来的空间复杂度和时间复杂度。使用展开图分析Petri网的行为属性与传统的Petri网分析方法相比，具有自己的特点。该文首先介绍了Petri网展开图的构造算法，在此基础上使用展开图分析方法对一个典型Petri网的活性，有界性和可逆性等行为属性进行了分析，并与传统的Petri网分析方法作比较。     

基于库所指标分解的Petri网活性与公平性分析

Petri网的分解技术是用于复杂网系统分析的一种有效手段．基于库所指标的Petri网分解方法，将一个复杂的网系统分解成结构简单的子网，分解后的子网保持原网系统的语言行为不变当且仅当具有公共变迁的子网的可达图关于公共变迁是同构的．若分解过程中保持系统的语言行为不变，则在Petri网的活性和公平性方面有着对应关系．本文基于分解给出了Petri网活性判定的充要条件和公平性判定的定理，对基于分解的复杂系统的Petri网分析方法提供了更为有效的理论和可行的技术．     

基于变迁指标分解的Petri网性质分析

Petri网的分解技术是复杂网系统分析的一种重要手段,基于变迁指标的分解方法将系统分解为一组T-网。通过获得分解子网的结构性质以及子网与原网间的性质保持关系,得到了判定原网结构性质的一些方法和结论;同时给出了判定原网系统活性的一个条件。所得结果为结构复杂Petri网的性质分析提供了有效的方法。     

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     

The use of Petri Nets for Occam programming for transputers

There is undoubtedly a need for software-design tools for parallel programming. A main problem with design tools for parallel programming is their inability to check for liveness (no deadlock) and safeness. In this paper, the use of Ordinary Petri net as a software design tool for Occam Petri Net and Occam constructs are discussed. The similarities between Ordinary Petri Net and Occam constructs are highlighted, and an Occam Petri Net model is proposed as a design tool to aid in writing Occam codes. The Occam Petri Net model is graphical. It is capable of modelling deterministic concurrent and choice systems. As a top-down design, the net is similar to Occam ‘folds’, and, in its use in bottom-up implementation, it is similar to unfolding. This unfolding using the Occam Petri Net model makes writing Occam source codes easier. The availability of Petri Net CASE tools will make it more attractive for designing Occam programs.     

T-网的活性分析及其判断算法

Petri网的活性反映了实际系统的元死锁性.本文讨论了一类结构简单的Petri网-T-网的活性问题,给出了各类T-网的活性判定定理并给出了判定算法.算法主要计算工作是变迁的前序库所集和后继变迁集以及回路的判断,这三个过程实际上是一个树的搜索过程,因此算法易于实现,判定效率也大大提高.     

Automatic construction of systems of distributed components from nested Petri nets models

Multi-level multi-agent systems (MASs) with dynamic structure are widely used in solving important applied problems in telecommunication, transportation, social, and other systems. Therefore, ensuring correct behavior of such systems is an actual and important task. One of the most error-prone stages of system development in the framework of model-oriented approach is the implementation stage, in the course of which a program code is constructed based on the model developed. This paper presents an algorithm for automated translation of MAS models represented as nested Petri nets into systems of distributed components. Nested Petri nets are the extension of Petri nets in the framework of the nets-within-nets approach, which assumes that tokens in a Petri net may themselves be Petri nets, possess autonomous behavior, and interact with other tokens of the net. This makes it possible to model MASs with dynamic structure in a natural way. The translation presented in this paper preserves distribution level and important behavioral properties (safety, liveness, and conditional liveness) of the original model and ensures fairness of the target system execution. The use of such translation makes it possible to automate construction of distributed MASs by models of nested Petri nets. As a test example, translation of nested Petri nets into systems of distributed components was implemented on the basis of the EJB component technology.     

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.     

无冲突Petri网的结构活性判定研究

结构活性作为Petri网的重要结构性质,在Petri网活性判定领域具有较高的研究价值。从Petri网有向回路对结构活性的影响入手,分析与判定无冲突Petri网的结构活性,讨论库所元素及其后置变迁之间是否存在有向回路对Petri网结构活性的影响,研究该类Petri网结构活性判定方法的相关条件与结论,得到无冲突Petri网是满足结构活性的充分必要条件。分析结果表明,该判定方法可在多项式时间内判定无冲突Petri网的结构活性。     

Timed Petri Nets in Hybrid Systems: Stability and Supervisory Control

In this paper, timed Petri nets are used to model and control hybrid systems. Petri nets are used instead of finite automata primarily because of the advantages they offer in dealing with concurrency and complexity issues. A brief overview of existing results on hybrid systems that are based on Petri nets is first presented. A class of timed Petri nets named programmable timed Petri nets (PTPN) is then used to model hybrid systems. Using the PTPN, the stability and supervisory control of hybrid systems are addressed and efficient algorithms are introduced. In particular, we present sufficient conditions for the uniform ultimate boundness of hybrid systems composed of multiple linear time invariant plants which are switched between using a logical rule described by a Petri net. This paper also examines the supervisory control of a hybrid system in which the continuous state is transfered to a region of the state space in a way that respects safety specifications on the plant's discrete and continuous dynamics.     

基于Petri网语言的并发系统性质研究

给出Petri网弱活性（无死锁）与活性的两个语言刻画,讨论了同步合成Petri网的语言性质,基于Petri网语言,给出了判定Petri网活性的充分必要条件。同时研究了Petri网同步合成过程中活性保持问题,给出保持活性的充分必要条件。这些结果为讨论网的活性测试和控制提供了形式语言的方法。     

公平网的活性判断

Petri网的活性判断一直是一个广为关心的问题。本文就公平网的活性进行了研究。指出如果一个公平网的有界子网是活的,那么该公平网是活的。并给出了一个公平网活的充分必要条件。     

Liveness Problem of Petri Nets Supervisory Control Theory for Discrete Event Systems

A quite great progress of the supervisory control theory for discrete event systems (DES) has been made in the past nearly twenty years, and now, automata, formal language and Petri nets become the main research tools. This paper focus on the Petri nets based supervisory control theory of DES. Firstly, we review the research results in this field, and claim that there generally exists a problem in Petri nets based supervisory control theory of DES, that is, the deadlock caused by the controller introduced to enforce the given specification occurs in the closed-loop systems, especially the deadlock occurs in the closed-loop system in which the original plant is live. Finally, a possible research direction is presented for the solution of this problem.     

Petri网极小虹吸的计算方法与性能分析

虹吸是Petri网的一种重要结构,可以用来分析所模拟系统的许多重要特性,如可达性、可逆性和活性等.文中首先提出了虹吸子网的概念,并给出了将Petri网划分成虹吸子网的多项式算法,进而给出其性能分析.通过求解虹吸子网的极小虹吸得到原Petri网的所有极小虹吸.而对于每个虹吸子网,首先求解它的一个极小虹吸,并根据此极小虹吸对子网进行分解,将分解得到的子网做类似原网的处理过程,直到每个子网的位置集就是一个极小虹吸或不包含任何极小虹吸为止.性能分析及实验表明,所构造的求解Petri网所有极小虹吸的算法是一个有效的算法.     

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 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).