Overlapping decompositions and expansions of Petri nets

Overlapping decompositions and expansions are considered to design decentralized controllers for discrete-event systems (DESs) modeled by Petri nets. The inclusion principle for Petri nets is first defined. It is shown that properties like boundedness, reversibility, and liveness (with a mild additional condition) carry over from the including net to the included net. Moreover, a new property called obstruction, is introduced for the including net, and it is shown that if obstruction does not occur in the including net, then deadlock does not occur in the included net. An expansion procedure, which guarantees inclusion for an overlappingly decomposed Petri net, is then introduced     

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.     

Concurrency bugs in multithreaded software: modeling and analysis using Petri nets

In this paper, we apply discrete-event system techniques to model and analyze the execution of concurrent software. The problem of interest is deadlock avoidance in shared-memory multithreaded programs. We employ Petri nets to systematically model multithreaded programs with lock acquisition and release operations. We define a new class of Petri nets, called Gadara nets, that arises from this modeling process. We investigate a set of important properties of Gadara nets, such as liveness, reversibility, and linear separability. We propose efficient algorithms for the verification of liveness of Gadara nets, and report experimental results on their performance. We also present modeling examples of real-world programs. The results in this paper lay the foundations for the development of effective control synthesis algorithms for Gadara nets.     

一种三态加时变迁Petri网的形式化描述与分析

提出一种弱引发规则三态加时变迁Ｐｅｔｒｉ网（简称ＷＴＴＰＮ），它比现有三态加时变迁Ｐｅｔｒｉ网更适于建模分析冲突结构；平行于无时间约束Ｐｅｔｒｉ网，给出了并发意义下ＷＴＴＰＮ的形式化描述与分析框架，据此可对其进行定性分析；证明了ＷＴＴＰＮ与其基网系统关于活性、有界（安全）性和可逆性等价。     

一类FMS的最佳活Petri网模型的综合

利用Petri网为一类柔性制造系统建模,并讨论避免系统死锁问题.通过Petri网模 型的结构分析,证明了系统产生死锁的一个充分必要条件.给出了避免死锁的最佳控制器,它 可以通过给系统的Petri网模型增加一些新的位置与相应的弧来实现.从而导出了这类制造 系统的最佳活Petri网模型.     

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

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

Petri网精细化操作及其在系统设计中的应用

针对柔性制造系统的设计问题,提出了用Petri网精细化操作解决问题的方案.给出了两种精细化操作.研究了Petri网精细化操作的动态性质保持问题,给出了精细化操作保持活性、有界性、可回复性的充分必要条件;对一个柔性制造系统进行了设计和验证.其结果可为Petri网系统静态和动态性质的考察提供有效途径,为Petri网复杂大系统的分析提供重要手段,并特别适合于柔性制造系统的设计,具有一定的实用价值.     

Petri网的PP型子网精细化操作性质分析及应用

针对工厂用车间中的若干台机器加工某些部件等这一类业务处理问题，提出了用Petri网精细化操作解决问题的方案。定义了一种PP型子网，用这种子网分别对Petri网系统中的某些库所进行细化，得到更细致、更精确的Petri网系统。研究了Petri网精细化操作的动态性质保持问题，给出这种精细化操作保持活性、有界性、可回复性和公平性的充要条件；本文的结果可为Petri网系统静态和动态性质的考察提供有效途径，为Petri网复杂大系统的分析提供重要手段，并特别适合于一类业务系统的描述和处理，具有一定的实用价值。     

Structure and behavior preservation by Petri-net-based refinements in system design

A refinement is a transformation for replacing a simple entity of a system with its functional and operational details. In general, the refined system may become incorrect even if the original system is correct because some of its original properties may have been lost or some unneeded properties may have been created. For systems specified in pure ordinary Petri nets, this paper proposes the conditions imposed on several types of refinement under which the following 19 properties will be preserved: state machine, marked graph, free choice net, asymmetric choice net, conservativeness, structural boundedness, consistence, repetitiveness, rank, cluster, rank-cluster-property, coverability by minimal state-machines, siphon, trap, cyclomatic complexity, longest path, boundedness, liveness and reversibility. Such results have significance in three aspects: (1) It releases the designer's burden for having to provide different methods for individual properties. (2) In the literature, refinements have been shown preserving several equivalence relations and behavioral properties. Our results show that they also preserve many structural properties. (3) It greatly enlarges the scope of applicability of refinements because they can now be applied on systems that satisfy more properties than just liveness and boundedness.     

Non‐blocking decentralized control of discrete event systems based on Petri nets

The non‐blocking property of discrete event systems can formulate many practical and important properties of manufacturing systems, such as deadlock freeness, liveness and reversibility. But it is difficult to guarantee non‐blocking control. This paper presents a hybrid approach to decentralized control of discrete event systems. More generalized constraints are considered in this approach, which gives a graphical way of designing coordinators to keep the non‐blocking property of the closed‐loop system with decentralized supervisors. This approach also guarantees that the closed‐loop system is maximally permissive. Copyright © 2010 John Wiley and Sons Asia Pte Ltd and Chinese Automatic Control Society     

Petri网的TT型子网精细化操作性质分析及其应用

针对企业用加工厂或车间加工某种产品等这一类业务处理问题，提出了用Petri网精细化操作解决问题的方案。定义了一种TT-型子网，用这种子网分别对Petri网系统中的某些变迁进行细化，得到更细致、更精确的Petri网系统。研究了Petri网精细化操作的动态性质保持问题，给出这种精细化操作保持活性、有界性、可回复性和公平性的充要条件；本文的结果可为Petri网系统静态和动态性质的考察提供有效途径，为Petri网复杂大系统的分析提供重要手段，并特别适合于一类业务系统的描述和处理，具有一定的实用价值。     

Petri网共享T型子网合成结构性质分析及其应用

为了解决系统设计中的子系统共享问题，提出了经由Petri网共享T-型子网构成共享T-型子网合成网的解决方案；研究了共享T-型子网合成网的结构性质，提出了共享T-型子网合成网保持结构有界性、守恒性、可重复性、相容性、P-不变量、T-不变量、公平性和结构活性的充分条件或充要条件；特别在证明结构活性保持性的过程中，体现了Petri网层次化的描述方法。本文的结果可为Petri网系统合成性质的考察提供有效途径，为复杂大系统的分析提供重要手段，并特别适合于一类系统的设计和分析，具有一定的实用价值。     

A Reduced Reachability Tree for a Class of Unbounded Petri Nets

As a powerful analysis tool of Petri nets, reachability trees are fundamental for systematically investigating many characteristics such as boundedness, liveness and reversibility. This work proposes a method to generate a reachability tree, called ωRT for short, for a class of unbounded generalized nets called ω-independent nets based on new modified reachability trees (NMRTs). ωRT can effectively decrease the number of nodes by removing duplicate and ω-duplicate nodes in the tree, and verify properties such as reachability, liveness and deadlocks. Two examples are provided to show its superiority over NMRTs in terms of tree size.      

Petri网化简操作及其在系统验证中的应用

针对柔性制造系统的验证问题，提出了用Petri网化简操作解决问题的方案。给出了两种化简操作。研究了这两种化简操作的动态性质保持问题，给出了化简后的Petri网保持活性、有界性、可回复性的一组充分条件或充要条件。对一个柔性制造系统进行了验证。本文的结果可为Petri网系统静态和动态性质的考察提供有效途径，为复杂大系统的分析提供重要手段，并特别适合于柔性制造系统的验证，具有一定的实用价值。     

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.     

基于共享位置的Petri网系统综合与保性

基于Petri网技术及其共享位置(shared places),文章介绍了一种综合设计方法,该方法便于多种设计模型的重用,并且在一定条件下,每一步综合设计过程都能保持无死锁(deadlock free)等Petri网的重要行为特点.对一些特殊的网类,活性(liveness)也能保持.     

Some subclasses of Petri nets and the analysis of their structuralproperties: a new approach

The purpose of the paper is to consider some special types of Petri nets, introduced by Lien (1976), and to propose a complete and unified approach for the study of their structural properties by using techniques of linear algebra of matrices. We distinguish four subclasses: forward-conflict-free, backward-conflict-free, forward-concurrent-free, and backward-concurrent-free Petri nets. A modification of the classical incidence matrix results in a square matrix, called a modified incidence matrix, with nonpositive (nonnegative) off-diagonal elements when backward-(forward-) conflict-free or concurrent-free Petri nets are considered. The modified incidence matrix eigenvalues are computed and theorems on matrices of this type are used to prove several sufficient and/or necessary conditions for structural boundedness, liveness, repetitiveness, conservativeness, and consistency of these four subclasses of Petri nets     

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.     

On systematic methods to remove redundant monitors from liveness-enforcing net supervisors

Petri nets based deadlock prevention for flexible manufacturing systems has received much attention over the past decade, primarily due to the seminal work of Ezpeleta et al. in 1995. A Petri net based deadlock prevention mechanism is usually implemented by adding monitors or control places to a plant Petri net model such that liveness can be enforced. The significance of this methodology lies in that both a plant model and its supervisor are in a same formalism-Petri nets. Due to the inherent complexity of Petri nets, in theory, the number of additional monitors that have to been added to achieve liveness-enforcement purpose for an uncontrolled plant model is exponential with respect to the size of the model. This paper first proposes a systematic method to minimize the number of additional monitors in a liveness-enforcing Petri net supervisor such that the resultant net system has the same permissive behavior while liveness can still be preserved. Furthermore, for the liveness-enforcing Petri net supervisors of flexible manufacturing systems, which have some particular property, an algorithm is developed such that more permissive liveness-enforcing Petri net supervisors can be obtained after liveness-restrictive monitor removal. Compared with the existing techniques of eliminating redundant monitors in the literature, the complete state enumeration of a supervisor is avoided, which implies the high computational efficiency of the methods in this paper. Flexible manufacturing examples are used to demonstrate the proposed approaches.