Well-structured languages

This paper introduces the notion of well-structured language. A well-structured language can be defined by a labelled well-structured transition system, equipped with an upward-closed set of accepting states. That peculiar class of transition systems has been extensively studied in the field of computer-aided verification, where it has direct an important applications. Petri nets, and their monotonic extensions (like Petri nets with non-blocking arcs or Petri nets with transfer arcs), for instance, are special subclasses of well-structured transition systems. We show that the class of well-structured languages enjoy several important closure properties. We propose several pumping lemmata that are applicable respectively to the whole class of well-structured languages and to the classes of languages recognized by Petri nets or Petri nets with non-blocking arcs. These pumping lemmata allow us to characterize the limits in the expressiveness of these classes of language. Furthermore, we exploit the pumping lemmata to strictly separate the expressive power of Petri nets, Petri nets with non-blocking arcs and Petri nets with transfer arcs.     

Integer Linear Programming and the Analysis of Some Petri Net Problems

A class of Petri nets (called type \cal L Petri nets in this paper) whose reachability sets can be characterized by integer linear programming is defined. Such Petri nets include the classes of conflict-free , normal , BPP , trap-circuit , and extended trap-circuit Petri nets, which have been extensively studied in the literature. We demonstrate that being of type \cal L is invariant with respect to a number of Petri net operations, using which Petri nets can be pieced together to form larger ones. We also show in this paper that for type \cal L Petri nets, the model checking problem for a number of temporal logics is reducible to the integer linear programming problem, yielding an NP upper bound for the model checking problem. Our work supplements some of the previous results concerning model checking for Petri nets. Received October 1997, and in revised form July 1998.     

Supervisor synthesis for discrete event systems under partial observation and arbitrary forbidden state specifications

In this paper, we consider the forbidden state problem in discrete event systems modeled by partially observed and partially controlled Petri nets. Assuming that the reverse net of the uncontrollable subnet of the Petri net is structurally bounded, we compute a set of weakly forbidden markings from which forbidden markings can be reached by firing a sequence of uncontrollable/unobservable transitions. We then use reduced consistent markings to represent the set of consistent markings for Petri nets with structurally bounded unobservable subnets. We determine the control policy by checking if the firing of a certain controllable transition will lead to a subsequent reduced consistent marking that belongs to the set of weakly forbidden markings; if so, we disable the corresponding controllable transition. This approach is shown to be minimally restrictive in the sense that it only disables behavior that can potentially lead to a forbidden marking. The setting in this paper generalizes previous work by studying supervisory control for partially observed and partially controlled Petri nets with a general labeling function and a finite number of arbitrary forbidden states. In contrast, most previous work focuses on either labeling functions that assign a unique label to each observable transition or forbidden states that are represented using linear inequalities. More importantly, we demonstrate that, in general, the separation between observation and control (as considered in previous work) may not hold in our setting.     

Petri Nets as Semantic Domain for Diagram Notations

This paper summarizes the work carried out by the authors during the last years. It proposes an approach for defining extensible and flexible formal interpreters for diagram notations based on high-level timed Petri nets.The approach defines interpreters by means of two sets of rules. The first set specifies the correspondences between the elements of the diagram notation and those of the semantic domain (Petri nets); the second set transforms events and states of the semantic domain into visual annotations on the elements of the diagram notation. The feasibility of the approach is demonstrated through MetaEnv, a prototype tool that allows users to implement special-purpose interpreters.     

On enumerating minimal siphons in Petri nets using CLP and SAT solvers: theoretical and practical complexity

Petri nets are a simple formalism for modeling concurrent computation. They are also an interesting tool for modeling and analysing biochemical reaction systems, bridging the gap between purely qualitative and quantitative models. Biological networks can indeed be complex, large, and with many unknown kinetic parameters, which makes the development of quantitative models difficult. In this paper, we focus on the Petri net representation of biochemical reactions and on two structural properties of Petri nets, siphons and traps, that bring us information about the persistence of some molecular species, independently of the kinetics. We first study the theoretical time complexity of minimal siphon decision problems in general Petri nets, and present three new complexity results: first, we show that the existence of a siphon of a given cardinality is NP-complete; second, we prove that deciding the Siphon-Trap property is co-NP-complete; third, we prove that deciding the existence of a minimal siphon containing a given set of places, deciding the existence of a siphon of a given cardinality and deciding the Siphon-Trap property can be done in linear time in Petri nets of bounded tree-width. Then, we present a Boolean model of siphons and traps, and two method for enumerating all minimal siphons and traps of a Petri net, by using a SAT solver and a Constraint Logic Program (CLP) respectively. On a benchmark of 345 Petri nets of hundreds of places and transitions, extracted from biological models from the BioModels repository, as well as on a benchmark composed of 80 Petri nets from the Petriweb database of industrial processes, we show that both the SAT and CLP methods are overall faster by one or two orders of magnitude compared to the state-of-the-art algorithm from the Petri net community, and are in fact able to solve all the enumeration problems of our practical benchmarks. We investigate why these programs perform so well in practice, and provide some elements of explanation related to our theoretical complexity results.     

Recursive Petri nets

In order to design and analyse complex systems, modelers need formal models with two contradictory requirements: a high expressivity and the decidability of behavioural property checking. Here we present and develop the theory of such a model, the recursive Petri nets. First, we show that the mechanisms supported by recursive Petri nets enable to model patterns of discrete event systems related to the dynamic structure of processes. Furthermore, we prove that these patterns cannot be modelled by ordinary Petri nets. Then we study the decidability of some problems: reachability, finiteness and bisimulation. At last, we develop the concept of linear invariants for this kind of nets and we design efficient computations specifically tailored to take advantage of their structure.     

基于有色网的多Agent计划建模

有色网能够描述资源和操作的具体语义。首先,由于计划中的操作和状态的个数的有限性,与有色网的元素个数有限性约束完全一致。另外,计划中的动作与有色网中的变迁语义类似,以及计划中的操作和状态和有色网中的库所语义非常类似。因此,有色网应用到计划的形式化中,有其独特的优势。本文根据约定的前提条件,计划建模从操作、状态和交互3个方面来具体实现,并给出了建模方法。计划的规范描述、有效性验证以及计划的模拟都可以直接应用经典Petri网或有色网的理论技术。     

Some decision problems related to the reachability problem for Petri nets

In this paper, we show that (1) the question to decide whether a given Petri net is consistent, M_o-reversible or live is reduced to the reachability problem in a unified manner, (2) the reachability problem for Petri nets is equivalent to the equality problem and the inclusion problem for the sets of all firing sequences of two Petri nets, (3) the equality problem for the sets of firing sequences of two Petri nets with only two unbounded places under homomorphism is undecidable, (4) the coverability and reachability problems are undecidable for generalized Petri nets in which a distinguished transition has priority over the other transitions, and (5) the reachability problem is undecidable for generalized Petri nets in which some transitions can reset a certain place to zero marking.     

信标基底的可选择性在制造系统死锁控制中的应用

本文基于Petri网模型,讨论柔性制造系统的死锁控制问题.为了建立结构简单的Petri网控制器,本文在以前的工作中提出了信标基底的概念.信标基底是一组满足特定条件的严格极小信标集合.本文证明基于不同的信标基底,建立的受控系统其容许性能也不同.而容许性是评价死锁控制策略优劣的重要标准之一.故如何选择信标基底,提高受控系统的容许性能是值得研究的问题.本文讨论了使受控系统容许性能大大提高的信标基底的选择条件.基于该条件,为柔性制造系统建立有效的死锁控制策略.最后,通过两个例子解释该条件和策略.     

Normal Petri nets

A class of Petri nets, called normal Petri nets, is introduced, and it is shown that, for each initial marking, the reachability set of a normal marked Petri net is an effectively computable semilinear set. More generally, we show that the reachability set of a marked Petri net is an effectively computable semilinear set unless the total number of tokens in a minimal circuit is decreased to 0. We also show that a Petri net is normal if and only if it is weakly persistent for each initial marking without token-free circuits.     

Decidability results in First–Order Hybrid Petri Nets

In this paper we tackle the decidabilityof marking reachability for a hybrid formalism based on Petrinets. The model we consider is the untimed version of First–OrderHybrid Petri Nets: it combines a discrete Petri net and a continuousPetri net, the latter being a fluid version of a usual discretePetri net. It is suggested that the decidability results shouldbe pursued exploiting a hierarchy of models as it has been donein the framework of Hybrid Automata. In this paper we definethe class of Single–Rate Hybrid Petri Nets: the continuousdynamics of these nets is such that the vector of the markingderivatives of the continuous places is constant but for a scalarfactor. This class of nets can be seen as the counterpart oftimed automata with skewed clocks. We prove that the reachabilityproblem for this class can be reduced to the reachability problemof an equivalent discrete net and thus it is decidable.     

Elementary siphons of Petri nets and their application to deadlock prevention in flexible manufacturing systems

A variety of important Petri net-based methods to prevent deadlocks arising in flexible manufacturing systems (FMS) are to add some control places and related arcs to strict minimal siphons (SMS) such that no siphon can be emptied. Since the number of minimal siphons grows in general exponentially with respect to a Petri net size, their disadvantages lie in that they often add too many additional places to the net, thereby making the resulting net model much more complex than the original one. This paper explores ways to minimize the new additions of places while achieving the same control purpose. It proposes for the first time the concept of elementary siphons that are a special class of siphons. The set of elementary siphons in a Petri net is generally a proper subset of the set of all SMS. Its smaller cardinality becomes evident in large Petri net models. This paper proves that by adding a control place for each elementary siphon to make sure that it is marked, deadlock can be successfully prevented. Compared with the existing methods, the new method requires a much smaller number of control places and, therefore, is suitable for large-scale Petri nets. An FMS example is used to illustrate the proposed concepts and policy, and show the significant advantage over the previous methods.     

稳定有界Petri网的进程表达式

文献[1]证明一个有界Pctri网的进程表达式是以该网的基本子进程集为字母表的正规表达式,然而没有给出基本子进程的求解方法。定义了一类有界Petri网—稳定有界Petri网,并给出其基本子进程的求解算法,进而利用有限自动机的语言表达式的求解方法来求解稳定有界Pctri网的进程表达式。另外,还给出了由符合一定条件的导网的进程表达式来构造其同步合成网的进程表达式的算法。     

Extended Elementary Siphons and Their Application to Liveness‐Enforcement of Generalized Petri Nets

As a significant structural object, siphons are extensively employed to implement a large number of deadlock prevention and liveness‐enforcing methods for flexible manufacturing systems modeled by Petri nets. By linear combinations, a set of elementary siphons is chosen from all strict minimal ones to be controlled and thus the structural complexity of a supervisor is greatly reduced. The concept of elementary siphons is originally proposed for ordinary Petri nets. When applied to generalized Petri nets, their selection and controllability require an additional study. In this work, the concept of augmented siphons is proposed to extend the application of the elementary ones to a class of generalized Petri nets, GLS³PR. Based on graph theory, a siphon extraction algorithm is developed to obtain all strict minimal siphons, from which augmented elementary ones are computed. In addition, the controllability conditions of dependent siphons are developed. Through fully investigating the net structure, especially weight information, the set of augmented elementary siphons is more compact and well suits for generalized Petri net models under consideration. Some examples are used to illustrate the proposed method.     

SAT-Solving the Coverability Problem for Petri Nets

Net unfoldings have attracted great attention as a powerful technique for combating state space explosion in model checking, and have been applied to verification of finite state systems including 1-safe (finite) Petri nets and synchronous products of finite transition systems. Given that net unfoldings represent the state space in a distributed, implicit manner the verification algorithm is necessarily a two step process: generation of the unfolding and reasoning about it. In his seminal work McMillan (K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, 1993) showed that deadlock detection on unfoldings of 1-safe Petri nets is NP-complete. Since the deadlock problem on Petri nets is PSPACE-hard it is generally accepted that the two step process will yield savings (in time and space) provided the unfoldings are small.In this paper we show how unfoldings can be extended to the context of infinite-state systems. More precisely, we show how unfoldings can be constructed to represent sets of backward reachable states of unbounded Petri nets in a symbolic fashion. Furthermore, based on unfoldings, we show how to solve the coverability problem for unbounded Petri nets using a SAT-solver. Our experiments show that the use of unfoldings, in spite of the two-step process for solving coverability, has better time and space characteristics compared to a traditional reachability based implementation that considers all interleavings for solving the coverability problem.     

Decidability and complexity of Petri nets with unordered data

We prove several decidability and undecidability results for ν-PN, an extension of P/T nets with pure name creation and name management. We give a simple proof of undecidability of reachability, by reducing reachability in nets with inhibitor arcs to it. Thus, the expressive power of ν-PN strictly surpasses that of P/T nets. We encode ν-PN into Petri Data Nets, so that coverability, termination and boundedness are decidable. Moreover, we obtain Ackermann-hardness results for all our decidable decision problems. Then we consider two properties, width-boundedness and depth-boundedness, that factorize boundedness. Width-boundedness has already been proven to be decidable. Here we prove that its complexity is also non-primitive recursive. Then we prove undecidability of depth-boundedness. Finally, we prove that the corresponding “place version” of all the boundedness problems is undecidable for ν-PN. These results carry over to Petri Data Nets.     

On path dependent loss and switch crosstalk reduction in optical networks

Although optical multistage interconnection networks (OMINs) promise to meet the ever growing demands of communication networks and multiprocessor systems in fast communication, they suffer from challenges such as path dependent loss and switch crosstalk. In this paper, we propose an innovative approach for reducing not only the path dependent loss but also the number of switch crosstalks in OMINs. Our approach is centered upon modelling OMINs with Petri nets and using the P-invariants method to determine the minimum number of stages m_min that is sufficient to establish requested communication patterns in variable-stage OMINs. Being composed of the smallest number of stages and consequently directional couplers (or photonic switches), m_min-stage OMIN employs minimal structure and, therefore, path dependent loss and also number of switch crosstalks reach the least possible values in the realization of requested communication patterns.We prove that the size of Petri nets created in this work is in polynomial dependence on the problem size which alleviates memory consumption significantly and ascertains the fact that memory capacity and performance of modern computers are indeed sufficient to run our task. We also show that the complexity results obtained in this research improve similar results reported in our previous paper. We carry out a series of computer experiments to confirm the effectiveness of the proposed approach.     

New NP-Complete Problems in Performance Evaluation of Concurrent Systems Using Petri Nets

Timed Petri nets are useful in performance evaluation of concurrent systems. The maximum computation rate is achieved for minimal cycle time of timed Petri net. It is known that minimal cycle time problem for P-invariant Petri nets is NP-complete. In this paper we prove that the minimal cycle time problem, for non-P-invariant Petri nets and for a small subclass of P-invariant Petri nets called free-choice nets having live and safe marking, is NP-complete.     

Timed high-level nets

Petri nets have been widely used for modeling and analyzing concurrent systems. Several reasons contribute to their success: the simplicity of the model, the immediate graphical representation, the easy modeling of asynchronous aspects, the possibility of reasoning about important properties such as reachability, liveness, boundedness. However, the original model fails in representing two important features: complex functional aspects, such as conditions which rule the flow of control, and time. Due to that, two different classes of extensions of Petri nets have been proposed: high-level nets and timed Petri nets. High-level nets allow the representation of functional aspects in full details, but do not provide a means for representing time; on the other hand, timed Petri nets have been thought for time representation, but they do not provide a means for representing detailed functinal aspects. Thus, these two important aspects cannot be mastered together. In particular, it is difficult to express relationships between time and functional aspects.This paper investigates the relationships between high-level nets and timed Petri nets, thus extending a first set of results published in a previous paper, where a unifying Petri net based model for time representation has been proposed. It first recalls how time can be represented in a Petri net extension called ER nets, and assesses its generality. It then investigates the relationships of ER nets with the best known high-level nets. In particular it shows the overall equivalence of ER nets, Colored Petri nets and Predicate/Transition nets, and extends the mechanism for time representation introduced in ER nets to both Colored Petri nets and Predicate/Transition nets. It also shows that these models cannot be simplified without significantly constraining the timing aspects that can be modeled.     

自动制造系统Petri网的公平活性控制策略

基于Petri网的不变式理论,针对典型的自动制造系统,提出了Petri模型强制公平性 和活性的方法.首先,基于网论T-不变式的概念,把系统的网模型设计为一个公平网.此后,利 用P-不变式把一个公平网设计为一个活的且公平网.同时,提出了非冗余严格极小信标的概念, 大大简化了系统的分析与设计.一般说来,非冗余严格极小信标是系统严格极小信标一个小的 子集,尤其对于复杂系统的网模型.研究结果表明,只要使非冗余的严格极小信标受控,则系统 所有的严格极小信标就不会被清空.文中举例说明了这些控制方法的应用.研究结果适用于一 大类柔性制造系统,具有相当的普遍性.这种方法对于自动制造系统的调度设计也具有一定意义 和价值.