Steady-state performance evaluation of continuous mono-T-semiflow Petri nets

The number of states in discrete event systems can increase exponentially with respect to the size of the system. A way to face this state explosion problem consists of relaxing the system model, for example by converting it to a continuous one. In the scope of Petri nets, the firing of a transition in a continuous Petri net system is done in a real amount. Hence, the marking (state) of the net system becomes a vector of non-negative real numbers. The main contribution of the paper lies in the computation of throughput bounds for continuous Petri net systems with a single T-semiflow. For that purpose, a branch and bound algorithm is designed. Moreover, it can be relaxed and converted into a linear programming problem. Some conditions, under which the system always reaches the computed bounds, are extracted. The results related to the computation of the bounds can be directly applied to a larger class of nets called mono T-semiflow reducible.     

Fuzzy rule base systems verification using high-level Petri nets

In this paper, we propose a Petri nets formalism for the verification of rule-based systems. Typical structural errors in a rule-based system are redundancy, inconsistency, incompleteness, and circularity. Since our verification is based on Petri nets and their incidence matrix, we need to transform rules into a Petri nets first, then derive an incidence matrix from the net. In order to let fuzzy rule-based systems detect above the structural errors, we are presenting a Petri-nets-based mechanism. This mechanism consists of three phases: rule normalization, rules transformation, and rule verification. Rules will be first normalized into Horn clauses, then transform the normalized rules into a high-level Petri net, and finally we verify these normalized rules. In addition, we are presenting our approach to simulate the truth conditions which still hold after a transition firing and negation in Petri nets for rule base modeling. In this paper, we refer to fuzzy rules as the rules with certainty factors, the degree of truth is computed in an algebraic form based on state equation which can be implemented in matrix computation in Petri nets. Therefore, the fuzzy reasoning problems can be transformed as the liner equation problems that can be solved in parallel. We have implemented a Petri nets tool to realize the mechanism presented fuzzy rules in this paper.     

A new methodology for analyzing distributed systems modeled by petri nets

Distributed computing systems can be modeled adequately by Petri nets. The computation of invariants of Petri nets becomes necessary for proving the properties of modeled systems. This paper presents a two-phase, bottom-up approach for invariant computation and analysis of Petri nets. In the first phase, a newly defined subnet, called the RP-subnet, with an invariant is chosen. In the second phase, the selected RP-subnet is analyzed. Our methodology is illustrated with two examples viz., the dining philosophers' problem and the connection-disconnection phase of a transport protocol. We believe that this new method, which is computationally no worse than the existing techniques, would simplify the analysis of many practical distributed systems.     

The equality problem for vector addition systems is undecidable

We demonstrate the usefulness of Petri nets for treating problems about vector addition systems by giving a simple exposition of Rabin's proof of the undecidability of the inclusion problem for vector addition system reachability sets, and then proceed to show that the inclusion problem can be reduced to the equality problem for reachability sets.     

Isomorphisms Between Petr Nets and Dataflow Graphs

Dataflow graphs are a generalized model of computation. Uninterpreted dataflow graphs with nondeterminism resolved via probabilities are shown to be isomorphic to a class of Petri nets known as free choice nets. Petri net analysis methods are readily available in the literature and this result makes those methods accessible to dataflow research. Nevertheless, combinatorial explosion can render Petri net analysis inoperative. Using a previously known technique for decomposing free choice nets into smaller components, it is demonstrated that, in principle, it is possible to determine aspects of the overall behavior from the particular behavior of components.     

标识T-网中同步距离的计算

同步距离是刻画事件之间同步关系的一个重要的定量分析手段.由于同步距离的求解不仅和网的结构特征有关系,而且和网的初始标识也存在关系,因此到目前为止还没有一个很简洁易行的算法来求解一般Petri网的同步距离.然而,一些特殊的Petri网子类,如标识T-图、标识S-图的同步距离的计算已经有了较简洁的求解方法.对另一个Petri网子类--标识T-网给出了其同步距离的计算方法.标识T-网也可以直接通过网的结构和初始标识分布情况来得到变迁之间的同步距离,不需要考察网系统的运行,这就使得同步距离的求解简单易行.文中给出了相应的求解定理.     

基于Petri网的列控系统形式化分析方法

利用原型Petri网对列车控制系统建模难于实现,用带抑止弧的增广Petri网则可以较好地描述问题。将带抑止弧的增广Petri网作为计算模型,对列车控制系统的一些关键问题进行了建模并给出了两个控制子系统：车站调度子系统与区间运行子系统。车站调度子系统实现了对列车请求进入和驶离车站的协调控制,区间运行子系统则实现了闭塞区间的车辆的安全性控制、突发事件时(如遭遇雷击,信号丢失的情况发生等)的安全性处理和公路铁路交叉口的调度等。最后,利用S-不变量对模型的活性、可达性和有界性等给予了形式化的验证。     

线性定常系统的Petri网解耦控制

将Petri网与现代控制理论相结合,应用于连续系统的性能分析如可控性、可观性和稳定性等已日益普遍,但Petri网应用于系统的解耦控制研究很少.提出了广义连续自控网系统的形式化定义,描述了线性定常系统的广义连续自控网系统模型并分析了广义连续自控网系统模型与状态空间描述的等效性.基于状态反馈动态解耦的基本原理,探讨了利用Petri网模型结构实现线性定常系统解耦控制的新方法.该方法采用图的遍历算法,可有效的判断系统的可解耦性以及实现解耦控制律,避免了传统解耦控制方法中计算所需的大量矩阵运算.最后给出了两个具体的应用实例.     

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.     

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.     

一类受控Petri网的基于管程的广义互斥控制

本文讨论受控Ｐｅｔｒｉ网的广义互斥控制问题。首先，我们给出了此问题存在管程最小约束控制解的充要条件，然后，对一类其不可控 子网为有限状态机的受控Ｐｅｔｒｉ网，证明了其广义互斥控制问题总存在管程最小约束控制解，并给出了综合这一管程的控制的算法。     

A characterization of the stochastic process underlying astochastic Petri net

Stochastic Petri nets (SPN's) with generally distributed firing times can model a large class of systems, but simulation is the only feasible approach for their solution. We explore a hierarchy of SPN classes where modeling power is reduced in exchange for an increasingly efficient solution. Generalized stochastic Petri nets (GSPN's), deterministic and stochastic Petri nets (DSPN's), semi-Markovian stochastic Petri nets (SM-SPN's), timed Petri nets (TPN's), and generalized timed Petri nets (GTPN's) are particular entries in our hierarchy. Additional classes of SPN's for which we show how to compute an analytical solution are obtained by the method of the embedded Markov chain (DSPN's are just one example in this class) and state discretization, which we apply not only to the continuous-time case (PH-type distributions), but also to the discrete case     

On the line planning problems of the hub public-transportation networks

This paper deals with the problem of line planning that is often posed in the public-transportation planning process. Centred on the hub-based networks, two important phases of this process are treated: the determination of lines and the computation of their frequencies. These two phases are performed to minimize connection times, which is one of the main characteristics of service parameters. As a mathematical tool, we use generalized stochastic Petri nets, which allow performance to be evaluated. It is shown that the Petri net modelling is a powerful technique used to study public-transport systems to assist in the decision-making process. Examples are outlined to illustrate the results.     

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

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

Piecewise constant timed continuous PNs for the steady state estimation of stochastic PNs

Reliability analysis is often based on stochastic discrete event models like Markov models or stochastic Petri nets. For complex dynamical systems with numerous components, analytical expressions of the steady state are tedious to work out because of the combinatory explosion with discrete models. The computation of numerical approximations is also time consuming due to the slow convergence of stochastic simulations. For these reasons, fluidification can be investigated to estimate the asymptotic behaviour of stochastic processes. The contributions of this paper are to point out that timed continuous Petri nets may lead to biased estimators of the stochastic steady state and to introduce fluid Petri nets with piecewise-constant maximal firing speeds and sufficient conditions in order to obtain unbiased estimators.     

Augmented reachability trees for 1-place-unbounded generalizedPetri nets

An augmented reachability tree (ART) is proposed to extend the capability of the classical reachability tree (RT) for analyzing qualitative properties, such as liveness, of a class of unbounded generalized Petri nets, called 1-place-unbounded nets, where there is at most one unbounded place for each net. The idea is based on the computation of the minimal marking of each node in the tree. An algorithm for obtaining the minimal marking is shown. Examples are given to illustrate the technique. In addition to liveness, the proposed method can verify other properties such as reversibility and feasible firing sequences. Furthermore, properties verifiable by RT are also verifiable by ART     

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.     

Invariant-preserving Petri net reduction and conditions for invariant-existence

The use of invariants is an important tool for analysis of distributed and concurrent systems modeled by Petri nets. For a large practical system, the computation of desired invariants by the existing techniques is a time-consuming task. This paper proposes a theoretical foundation for simplified computation of desired invariants. We provide invariant-preserving Petri net reduction rules followed by the conditions for the existence of invariants in various well-structured nets. If an invariant exists, it can be found directly from the net structure using the formulas derived, or by applying the existing techniques on the reduced net.     

Preserving Languages and Properties in Stepwise Refinement-Based Synthesis of Petri Nets

The current stepwise refinement operation of Petri nets mainly concentrates on property preservation, which is an effective way to analyze and verify complex systems. Further steps into this field are needed from the perspective of system synthesis and language preservation. First, the refinement of Petri nets is introduced based on a k-well-behaved Petri net, in which k tokens can be processed. Then, according to the different compositions of subsystems, well-, under- and overmatched refined Petri nets are proposed. In addition, the language and property relationships among sub-, original, and refined nets are studied to demonstrate behavior characteristics and property preservation in a system synthesis process. A manufacturing system is given as an example to illustrate the effectiveness of the proposed approach in synthesizing and analyzing the Petri nets of complex systems.