The synthesis problem of Petri nets

The synthesis problem of concurrent systems is the problem of synthesizing a concurrent system model from sequential observations. The paper studies the synthesis problem for elementary Petri nets and transition systems. A characterization of the class of transition systems which correspond to elementary Petri nets is proven. It is shown how to generate all elementary Petri nets corresponding to a given transition system. If there is any such elementary Petri net, it is proven that there always exists a small one which has only polynomially many elements in the size of the transition system. Received October 5, 1992 / April 11, 1995     

On the Regularity of Petri Net Languages

Petri nets are known to be useful for modeling concurrent systems. Once modeled by a Petri net, the behavior of a concurrent system can be characterized by the set of all executable transition sequences, which in turn can be viewed as a language over an alphabet of symbols corresponding to the transitions of the underlying Petri net. In this paper, we study the language issue of Petri nets from a computational complexity viewpoint. We analyze the complexity of theregularity problem(i.e., the problem of determining whether a given Petri net defines an irregular language or not) for a variety of classes of Petri nets, includingconflict-free,trap-circuit,normal,sinkless,extended trap-circuit,BPP, andgeneralPetri nets. (Extended trap-circuit Petri nets are trap-circuit Petri nets augmented with a specific type ofcircuits.) As it turns out, the complexities for these Petri net classes range from NL (nondeterministic logspace), PTIME (polynomial time), and NP (nondeterministic polynomial time), to EXPSPACE (exponential space). In the process of deriving the complexity results, we develop adecomposition approachwhich, we feel, is interesting in its own right, and might have other applications to the analysis of Petri nets as well. As a by-product, an NP upper bound of the reachability problem for the class of extended trap-circuit Petri nets (which properly contains that of trap-circuit (and hence, conflict-free) and BPP-nets, and is incomparable with that of normal and sinkless Petri nets) is derived.     

Priority conflict-free Petri nets

A number of problems concerning priority conflict-free Petri nets are investigated in this paper. We show the reachability problem for such Petri nets to be NP-complete. (Using a similar technique, the NP-completeness result applies to the class of priority BPP-nets as well.) As for the boundedness problem, an NP-completeness result is demonstrated for priority conflict-free Petri nets with two types of prioritized transitions. (In contrast, the problem is known to be P-complete for conflict-free Petri nets without priorities.) We also investigate the home state problem, i.e., the problem of determining whether home states exist in a given a Petri net, for conflict-free Petri nets with and without priorities. As it turns out, home states always exist for bounded conflict-free Petri nets without priorities. If an additional liveness constraint is imposed, such Petri nets are guaranteed to be ‘reversible’ (i.e., their initial states are home states). For priority conflict-free Petri nets, being bounded and live is sufficient for the existence of home states. However, if the liveness assumption is dropped, the existence of home states is no longer guaranteed. Received: 1 April 1997 / 8 December 1997     

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.     

Shrinking of Time Petri nets

The problem of the synthesis of time bounds enforcing good properties for reactive systems has been much studied in the literature. These works mainly rely on dioid algebra theory and require important restrictions on the structure of the model (notably by restricting to timed event graphs). In this paper, we address the problems of existence and synthesis of shrinkings of the bounds of the time intervals of a time Petri net, such that a given property is verified. We show that this problem is decidable for CTL properties on bounded time Petri nets. We then propose a symbolic algorithm based on the state class graph for a fragment of CTL. If the desired property “includes” k-boundedness, the proposed algorithm terminates even if the net is unbounded. A prototype has been implemented in our tool Romeo and the method is illustrated on a small case study from the literature.     

Complexity of some problems in Petri nets

We consider the complexity of several standard problems for various classes of Petri nets. In particular, the reachability problem, the liveness problem and the k-boundedness problems are analyzed. Some polynomial time and polynomial space complete problems for Petri nets are given. We then show that the problem of deciding whether a Petri net is persistent is reducible to reachability, partially answering a question of Keller. Reachability and boundedness are proved to be undecidable for the Time Petri net introduced by Merlin. Also presented is the concept of controllability, i.e., the capability of a set of transitions to disable a given transition. We show that the controllability problem requires exponential space, even for 1-bounded nets.     

基于Petri网合成与化简的分布式数据库系统并发控制的死锁检测

利用模块化设计的思想，首先为分布式数据库系统中各事务的每一种操作(读锁、写锁、解锁)构造一个基本的加权Petri网模型，并给出了加权Petri网共享合成的概念、然后利用共享合成技术，动态地构造各站点的加权Petri网模型，以适应系统的动态变化．此外，本文利用Petri网的化简技术，极大地简化了各站点的Petri网模型，之后利用同步合成技术构造出整个系统的Petri网模型，较好地解决了Petri网的可达性分析中可能出现的状态“爆炸”问题．最后给出了判断整个系统是否出现死锁的充分必要条件．     

Fault Detection and Diagnosis in Distributed Systems: An Approach by Partially Stochastic Petri Nets

We address the problem of alarm correlation in large distributed systems. The key idea is to make use of the concurrence of events in order to separate and simplify the state estimation in a faulty system. Petri nets and their causality semantics are used to model concurrency. Special partially stochastic Petri nets are developed, that establish some kind of equivalence between concurrence and independence. The diagnosis problem is defined as the computation of the most likely history of the net given a sequence of observed alarms. Solutions are provided in four contexts, with a gradual complexity on the structure of observations.     

Diagnosability of Petri nets with observation graphs

This paper addresses the problem of diagnosability for dynamic discrete event systems modeled with bounded or unbounded Petri nets that are deadlock-free and monitored with sensor configurations with marking and event measurements. The proposed method gives necessary and sufficient conditions for diagnosability. It is based on the transformation of the coverability graph into an observation graph that encodes all observation sequences of measured markings and events with respect to the sensor configuration. This graph also encodes all sequences of transitions that may fire from any reachable marking of the Petri net. Diagnosability is determined by analyzing the paths and circuits in the observation graph. The method is illustrated with several examples of bounded or unbounded Petri nets.     

Action Planning for Directed Model Checking of Petri Nets

Petri nets are fundamental to the analysis of distributed systems especially infinite-state systems. Finding a particular marking corresponding to a property violation in Petri nets can be reduced to exploring a state space induced by the set of reachable markings. Typical exploration(reachability analysis) approaches are undirected and do not take into account any knowledge about the structure of the Petri net. This paper proposes heuristic search for enhanced exploration to accelerate the search. For different needs in the system development process, we distinguish between different sorts of estimates.Treating the firing of a transition as an action applied to a set of predicates induced by the Petri net structure and markings, the reachability analysis can be reduced to finding a plan to an AI planning problem. Having such a reduction broadens the horizons for the application of AI heuristic search planning technology. In this paper we discuss the transformations schemes to encode Petri nets into PDDL. We show a concise encoding of general place-transition nets in Level 2 PDDL2.2, and a specification for bounded place-transition nets in ADL/STRIPS. Initial experiments with an existing planner are presented.     

Determinization of timed Petri nets behaviors

In this paper we are interested in sequentialization of formal power series with coefficients in the semiring \((\mathbb {R}\cup \{- \infty \},\max ,+)\) which represent the behavior of timed Petri nets. Several approaches make it possible to derive nondeterministic (max, + ) automata modeling safe timed Petri nets. Their nondeterminism is a serious drawback since determinism is a crucial property for numerous results on (max, + ) automata (in particular, for applications to performance evaluation and control) and existing procedures for determinization succeed only for restrictive classes of (max, + ) automata. We present a natural semi-algorithm for determinization of behaviors based on the semantics of bounded timed Petri nets. The resulting deterministic (max, + ) automata can be infinite, but a sufficient condition called strong liveness is proposed to ensure the termination of the semi-algorithm. It is shown that strong liveness is closely related to bounded fairness, which has been widely studied for Petri nets and other models for concurrency. Moreover, if the net cannot be sequentialized we propose a restriction of its logical behavior so that the sufficient condition becomes satisfied for the restricted net. The restriction is based on the synchronous product with non injectively labeled scheduler nets that are built in an incremental hierarchical way from simple scheduler nets.     

Discrete Time Stochastic Petri Nets

Basic graph models of processes, such as Petri nets, have usually omitted the concept of time as a parameter. Time has been added to the Petri net model in two ways. The timed Petri net (TPN) uses a fixed number of discrete time intervals. The stochastic Petri net (SPN) uses an exponentially distributed random variable. In this paper, a discrete time stochastic Petri model is described. These discrete time SPN's fill the gap between TPN and normal SPN. However, the use of discrete time complicates the SPN model in that more than one transition may fire at a time step. Finally, an example of a live and bounded Petri net which has nonempty, disjoint, recurrent subsets of markings is given.     

Framework for modeling and analysis of distributed problem-solving systems

Petri nets have the basic concepts necessary to model distributed systems with asynchronous processes. Petri nets are not directly applicable to certain kinds of systems like distributed intelligent systems (DISs). These are complex systems where multiple intelligent agents cooperate through communication to achieve the solution to a problem. The paper identifies the limitations of ordinary Petri nets for modeling DISs and proposes extensions. The extended Petri net incorporates colored tokens, inhibition arcs, non-primitive places and transitions, multiple copies of tokens and cumulative places. It is called a distributed problem-solving Petri net. The definitions and analysis techniques are given and illustrated by means of an example.     

Detection of Ada static deadlocks using Petri net invariants

A method is presented for detecting deadlocks in Ada tasking programs using structural; and dynamic analysis of Petri nets. Algorithmic translation of the Ada programs into Petri nets which preserve control-flow and message-flow properties is described. Properties of these Petri nets are discussed, and algorithms are given to analyze the nets to obtain information about static deadlocks that can occur in the original programs. Petri net invariants are used by the algorithms to reduce the time and space complexities associated with dynamic Petri net analysis (i.e. reachability graph generation)     

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.     

Modeling and analysis of timed Petri nets using heaps of pieces

The authors show that safe timed Petri nets can be represented by special automata over the (max, +) semiring, which compute the height of heaps of pieces. This extends to the timed case the classical representation a la Mazurkiewicz of the behavior of safe Petri nets by trace monoids and trace languages. For a subclass including all safe free-choice Petri nets, we obtain reduced heap realizations using structural properties of the net (covering by safe state machine components). The authors illustrate the heap-based modeling by the typical case of safe jobshops. For a periodic schedule, the authors obtain a heap-based throughput formula, which is simpler to compute than its traditional timed event graph version, particularly if one is interested in the successive evaluation of a large number of possible schedules     

时延Petri网分布式模拟的先行值研究

先行值计算是提高时延Petri网并行模拟性能的一个好的方法。给出了时延Petri网的先行值计算的四种基本结构,对于存在循环的复杂的Petri网结构给出了预测图算法,通过预测图,能够很容易求出静态和动态先行值,在并行模拟中利用先行值可以分析出存在并发和阻塞的结构,从而为网分块在并行机的结点上运行奠定了基础。     

Interacting behavioral Petri nets analysis for distributed causal model-based diagnosis

This paper deals with the problem of spatially distributed causal model-based diagnosis on interacting behavioral petri nets (BPNs). The system to be diagnosed comprises different interacting subsystems (each modeled as a BPN) and the diagnostic system is defined as a multi-agent system where each agent is designed to diagnose a particular subsystem on the basis of its local model, the local received observation and the information exchanged with the neighboring agents. The interactions between subsystems are captured by tokens that may pass from one net model to another via bordered places. The diagnostic reasoning scheme is accomplished locally within each agent by exploiting classical analysis techniques of Petri nets like reachability graph and invariant analysis. Once local diagnoses are obtained, agents begin to communicate to ensure that such diagnoses are consistent and recover completely the results that would be obtained by a centralized agent having a global view about the whole system. The paper concludes with an empirical comparison, in terms of the running time, of two implementations of Petri net analysis techniques used as a distributed diagnostic reasoning schemes.     

ST—组合Petri网的结构性质分析

本文提出ＳＴ－组合Ｐｅｔｒｉ网的概念,讨论了ＳＴ－组合Ｐｅｔｒｉ网对子网的结构性质保持问题,深入研究了ＳＴ－组合Ｐｅｔｒｉ网的结构活性、结构有界性,守恒性,可重复性,相容性,公平性。本文给出的网组合可作为系统合成与分析的有效方法。     

Can I find a partner? Undecidability of partner existence for open nets

We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of operability which we consider as fundamental as the successful notion of soundness for workflow nets, i.e., Petri net models of business processes and workflows. While we could give algorithmic solutions to the operability problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.