Reachability analysis in T-invariant-less Petri nets

An algorithm for reachability analysis in place/transition Petri nets having no transition invariants (T-invariants) is proposed. Given a Petri net with initial and target markings, a so-called complemented Petri net is created first that consists of the given Petri net and an additional complementary transition. Thereby, the reachability task is reduced to computation and investigation of those minimal-support and linearly combined T-invariants of the complemented Petri net, in which the complementary transition fires only once. Then, for each T-invariant with a single firing of the complementary transition, the algorithm will try to create a reachability path from the given initial marking to the target marking.     

Compositional generation of home states in free choice nets

Free choice nets are a class of Petri nets which allow the modelling of concurrency and nondeterministic choice, but with the restriction that choices cannot be influenced externally. Home states are initial states which lead to a strongly connected state graph, that is, a home state can be reached from any of its successor states. The main result of this paper characterises the home states of a well-formed free choice net compositionally by recourse to its decomposition into T-components.     

变迁耦合网的T-不变量求解算法

首先定义了变迁耦合网及相关概念,其次揭示了变迁耦合网N中各个分支网的T-不变量同N的T-不变量之间的关系,根据是否与耦合变迁有关,将N的极小T-不变量分为两类MTS1和MTS2,然后给出了变迁耦合网所有极小T-不变量的求解算法,并给出了两个简单例子加以说明,最后编程实现所提算法并给出初步实验数据.试验结果说明,本文所提算法比现有算法节省大量计算开支.     

关于ESAC网活性和有界性的一个多项式算法

寻找实际可行的多项式算法一直是Petri网应用的重要方面.给出了关于扩展强化非对称选择网(extended strong asymmetric choice nets,简称ESAC网)结构活和结构有界的一个判定算法.该算法可简单、有效地测试结构活结构有界的ESAC网的初始标识是否是活标识.ESAC网覆盖了自由选择网,因此,该算法应用范围较为广泛.     

Petri网共享单链子网合成及其应用研究

本文针对多个企业共用一个加工厂加工某种产品这一类业务处理问题,提出了经由Petri网共享单链子网构成单链子网合成网的解决方案;给出了自由选择网（FC）,非对称选择网（AC）的共享单链子网合成网为各自相应网的充分条件;提出了共享单链子网合成Petri网保持结构活性的条件;本文的结果可为Petri网系统合成的静态和动态性质的考察提供有效途径,具有宽广的应用前景.     

Performance Evaluation of Petri nets Centralized Implementation. The Execution Time Controller

The reaction time of a controller is a fundamental matter in discrete event control systems. Petri nets are extensively used in this field. The controller reads the inputs, executes the control Petri net and writes the output in a cyclic manner. The reaction time of this controller depends on the Petri net structure, on the events sequence and on the algorithm that executes the net. In this paper we present a performance evaluation of interpreted and centralized implementation techniques for ordinary Petri nets. Four techniques have been analyzed: brute force, enabled transitions, static representing places and dynamic representing places. The analysis has been carried out over a Petri net library composed of well know models which can be scaled using a parameter. The analysis of the results shows that the performance of the algorithms depends on the Petri net behavior (concurrency vs. effective conflicts).With the objective of minimizing the reaction time, we decided to design a Supervisor controller, which we have called execution time controller (ETC). The aim of the ETC is to determine in real time which algorithm executes the Petri net fastest and to change the execution algorithm when necessary. One possible application of the technique is the minimization of execution time of the programmable logic controllers programs developed in sequential function chart (SFC).     

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

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

Automating the Conversion of Colored Petri Nets with Qualitative Tokens Into Colored Petri Nets with Quantitative Tokens

The authors describe an algorithm for conversion of colored Petri nets with qualitative tokens into a colored Petri net with quantitative tokens preserving boundedness, mutual exclusion, and liveness properties. This conversion allows the invariance method to be applied to colored Petri nets, which uses the Truncated Set of Solutions finding algorithm for Petri net state equations expressed through systems of linear homogenous Diophantine equations. To show the algorithm’s efficiency, it is applied to the colored Petri net that models the operation of a grid system. Equivalence of net models is tested by constructing and analyzing equal finite-state machine.     

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.     

Performance modeling and analysis of workflow

Workflow model analysis is performed at logic, temporal, and performance levels. This paper mainly deals with the performance level issues. Workflow net (WF-net) is extended with time information to the timing workflow net (TWF-net). To provide a formal framework for modeling and analyzing workflow, this paper proposes a multidimension workflow net (MWF-net) that include multiple TWF-nets and the organization and resource information. The algorithm to decompose a free-choice and acyclic Petri nets (PN) into a set of T-components is extended to a TWF-net containing iteration structures. Then, resource availability and workload analysis is performed. A method for computing the lower bound of average turnaround time of transaction instances processed in a MWF-net is proposed. Finally a case study is used to show that the proposed method can be effectively utilized in practice.     

求有效极小（受控）可重复向量的一个算法

文献［１］基于有效（受控）可重复向量，给出了判定一个标准Ｐｅｔｒｉ网产生的语言分别为正规语言或上下文无关语言的充要条件，然而，求取一个标准Ｐｅｔｒｉ网的有效（受控）可重复向量是着定网语言属型的前提条件，文献［１］没有给出求取它们的方法，本文提出一个算法，使得文献［１］判据可实现，此外，作为副产品，同时产生出网的所有极小Ｔ－不变量以及公平性判定的实现。     

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

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

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.     

Synthesis a Petri net based control model for a FMS cell

Petri nets have been recognised as a high level formal and graphical specification language for modelling, analysis, and control of concurrent asynchronous distributed systems. This paper presents a PN model, synthesised by an extended version of the knitting synthesis technique. This method, as an incremental design approach, establishes the conditions under which the fundamental behavioural properties of the synthesised systems are fulfilled and preserved. That is, the synthesised models are live, bounded, and reversible (cyclic). A Petri net with the aforementioned properties is called a well-behaved Petri net system which is guaranteed to operate in a deadlock-free, stable, and cyclic fashion. Well-behaved Petri net models, synthesised using the proposed method can be compiled into control codes and implemented as real-time controllers for flexible manufacturing systems. The significance of this paper is due to the application of an extended version of knitting synthesis technique to a real life example of a flexible manufacturing system.     

Petri网用于Horn子句的逻辑推论

这篇论文探索了命题逻辑的Horn子句的Petri网模型,求解逻辑推论Petri网模型的T—不变量是求解逻辑推论的核心步骤,本文提供了计算T—不变量的算法,这些算法基于归约的思想,另外,在算法中利用单字母规则、纯字母规则和割裂规则可提高算法的速度和简化算法的复杂性。     

A synthesis technique of general petri nets

The general Petri net (GPN) is useful for modeling flexible manufacturing systems with multiple robots and workstations [15] and for parallel programs [8]. A problem of using reachability analysis for analyzing Petri nets (PN) is the large number of states generated. Most of the existing synthesis techniques do not deal with GPN. Koh et al.[15] invented a synthesis technique for GPN. We propose to improve their achievement by adding the simple Arc-ratio rules to Yaw's knitting technique [37, 38, 39] based on the notion of structure relationship together with new path generations, which mark the most distinct feature compared with other approaches. The synthesis rules and procedures of how to update the temporal matrix and structure synchronic distance are presented. The Arc-ratio rules for GPN are also presented. One can successfully synthesize complicated Petri nets using these rules. An example to synthesize a Petri net in [15] is illustrated. The correctness of each synthesis rule with an appropriate Arc-ratio rule for GPN is proved.     

Checking system boundedness using ordinary differential equations

Boundedness is one of the most important properties of discrete Petri nets. Determining the boundedness of a Petri net is usually done through building coverability graph or coverability tree. However, the computation is infeasible for complex applications because the size of the coverability graph may increase faster than any primitive recursive functions. This paper proposes a new technique to check the boundedness without causing this problem. Let a concurrent system be represented by a (discrete) Petri net. By relaxing the (discrete) Petri net to a continuous Petri net, we can model the concurrent system by a family of ordinary differential equations. It has been shown that the boundedness of the discrete Petri net is equivalent to the boundedness of the solutions of the corresponding ordinary differential equations. Hence, we can check the boundedness of a (discrete) Petri net by analyzing the solutions of a family of ordinary differential equations. A case study demonstrates the benefits of our technique.     

Logical inference of Horn clauses in Petri net models

Petri net models for the Horn clause form of propositional logic and of first-order predicate logic are studied. A net model for logical inconsistency check is proposed. Algorithms for computing T-invariants of Petri net models of logical inference systems are investigated. The algorithms are based on the idea of resolution and exploit the presence of one-literal, pure-literal, and splitting clauses to lead to faster computation. Algorithms for computing T-invariants of high-level Petri net (HLPN) models of predicate logic are presented     

可分解非对称选择网的活性和有界性

活性和有界性是网系统的重要行为特性.从分解以及尽可能简单分解的角度得到了非对称选择网的一个子类,可分解非对称选择网(简称DAC网),证明了DAC网系统活性的充分必要条件,同时给出了DAC网系统活性有界性的充分必要条件,也进一步讨论了判定一个Petri网系统是否是活的有界的DAC网系统的多项式算法.     

Reduction rules for time Petri nets

The goal of net reduction is to increase the effectiveness of Petri-netbased real-time program analysis. Petri-net-based analysis, like all reachabilitybased methods, suffers from the state explosion problem. Petri net reduction is one key method for combating this problem. In this paper, we extend several rules for the reduction of ordinary Petri nets to work with time Petri nets. We introduce a notion of equivalence among time Petri nets, and prove that our reduction rules yield equivalent nets. This notion of equivalence guarantees that crucial timing and concurrency properties are preserved.