Verification of causal models using petri nets

Many different approaches, mainly based on logical formalisms, have been proposed for modeling causal knowledge and the inferential mechanisms based on this type of knowledge. In this article we present an alternative approach to this problem in which the semantics of a causal model is provided by adopting Petri nets. We show how this scheme of modeling is powerful enough to capture all crucial aspects of the corresponding causal model, without resorting to very complex structures; indeed, the model is obtained using a particular type of deterministic Petri net. Moreover, a complete formalization of the aspects concerning the correctness of the represented causal model is provided in terms of reachability in the Petri net. We believe that this aspect is very important in the knowledge acquisition phase when precise correctness criteria should be defined and respected in the construction of the model. We analyze some of these criteria and we discuss an algorithm (based on a backward simulation of the net) capable of discovering incorrectness by exploiting analysis tools available for Petri nets and the explicit parallelism of the model. © 1992 John Wiley & Sons, Inc.     

DISTRIBUTED SIMULATION OF HIGH-LEVEL ALGEBRAIC PETRI NETS WITH LIMITED CAPACITY PLACES

The aim of this paper is to search for techniques to accelerate simulations exploiting the parallelism available in current multicomputers, and to use these techniques to study a class of Petri nets called high-level algebraic nets. These nets exploit the rich theory of algebraic specifications for high-level Petri nets. They also gain a great deal of modelling power by representing dynamically changing items as structured tokens whereas algebraic specifications turned out to be an adequate and flexible instrument for handling structured items. We focus on ECATNets (Extended Concurrent Algebraic Term Nets), a kind of high-level algebraic Petri nets with limited capacity places

Three distributed simulation techniques have been considered: asynchronous conservative, asynchronous optimistic and synchronous. These algorithms have been implemented in a network of workstations with MPI (Message Passing Interface). The influence that factors such as the characteristics of the simulated models, the organisation of the simulators and the characteristics of the target multicomputer have in the performance of the simulations have been measured and characterized

It is concluded that distributed simulation of ECATNets on a multicomputer system can in fact gain speedup over the sequential simulation, and this can be achieved even for small scale simulation models.     

Verification of Random Graph Transformation Systems

In this paper we describe some statistical results obtained by the verification of random graph transformation systems (GTSs). As a verification technique we use over-approximation of GTSs by Petri nets. Properties we want to verify are given by markings of Petri nets. We also use counterexample-guided abstraction refinement approach to refine the obtained approximation. A software tool (Augur) supports the verification procedure. The idea of the paper is to see how many of the generated systems can be successfully verified using this technique.     

基于高级Petri网的仿真剧情正规校核方法

针对仿真剧情主观校核不理想这一问题,提出了基于高级Petri网的仿真剧情正规校核方法．首先给出仿真剧情的形式化定义,并分析仿真剧情可能存在的错误类型;其次给出仿真剧情到高级Petri网的映射途径,并给出基于高级Petri网的仿真剧情校核准则和算法,此外,还给出实现仿真剧情动态校核的推理规则和机制;最后给出了一个正规校核工具框架．实际应用已经证明了该方法的有效性．     

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.     

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.     

延迟时间Petri网的验证分析

延迟时间Petri网（Delay Time Petri Nets，DTPN）是一类重要的时间扩展Petri网系统，解决了其他时间扩展Petri网（如时间Petri网）在保存时间约束时所面临的困难。可调度验证的目的是验证工作流模型时间约束的合理性，对流程实例的时间可达性进行仿真。提出一种基于DTPN的时间约束工作流验证分析方法。给出了DTPN的相关定义，并结合工作流控制结构描述了变迁可触发的时间条件；提出了DTPN触发点的概念以及基于此的验证分析算法；简要分析了DTPN的特性。DTPN的研究丰富完善了现有时间Petri网体系，具有积极的意义。     

Verifying time Petri nets by linear programming

The paper proposes an approach to solving some verification problems of time petri nets using linear programming.The approach is based on the observation that for loop-closed time Ptri nets,it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net.Using the technique the paper gives solutions to reachabiltiy and bounded delay timing analysis problems.For both problems algorithms are given,that are decision procedures for loop-closed time Petri nets.and semi-decision procedures for general time Petri nets.     

用UML与Petri网为智能代理建模

统一建模型语言（UML）已经成为软件系统的分析与设计的标准工具，但由它扩充而成的代理统一建模型语言（AUML）还没变成一个标准，目前的AUML规格说明还有很多的局限性，还不能胜任多代理系统的开发．Petri网是仿真、验证软件系统执行的正确性与有效性的形式化工具．本文主要分析当前AUML规格说明和Petri网概念．找出它们之间的结合点，提出用Petri网扩充AUML的方法．将其应用于多代理系统的开发，就能实施之前运用Petri网进行系统的正确性与有效性验证．     

Transformations of Petri Nets

The aim of this paper is an introduction to the area of Petri net transformations, a rule-based approach for dynamic changes of the net structure of Petri nets. This is especially important for the stepwise construction of Petri nets in the sense of the software development process in software engineering. The concept of Petri net transformations is based on that of graph transformations and high-level replacement systems and it is introduced within a small case study logistics.     

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.     

Verification of bounded Petri nets using integer programming

Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings—themselves a class of acyclic Petri nets—which contain enough information, albeit implicit, to reason about the reachable markings of the original Petri nets. In [19], a verification technique for net unfoldings was proposed, in which deadlock detection was reduced to a mixed integer linear programming problem. In this paper, we present a further development of this approach. The essence of the proposed modifications is to transfer the information about causality and conflicts between the events involved in an unfolding, into a relationship between the corresponding integer variables in the system of linear constraints. Moreover, we present some problem-specific optimisation rules, reducing the search space. To solve other verification problems, such as mutual exclusion or marking reachability and coverability, we adopt Contejean and Devie's algorithm for solving systems of linear constraints over the natural numbers domain and refine it, by taking advantage of the specific properties of systems of linear constraints to be solved. Another contribution of this paper is a method of re-formulating some problems specified in terms of Petri nets as problems defined for their unfoldings. Using this method, we obtain a memory efficient translation of a deadlock detection problem for a safe Petri net into an LP problem. We also propose an on-the-fly deadlock detection method. Experimental results demonstrate that the resulting algorithms can achieve significant speedups.

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.     

A high-level Petri nets-based approach to verifying task structures

As knowledge-based system technology gains wider acceptance, there is an increasing need to verify knowledge-based systems to improve their reliability and quality. Traditionally, attention has been given to verifying knowledge-based systems at the knowledge level, which only addresses structural errors such as redundancy, conflict and circularity in rule bases. No semantic errors (such as inconsistency at the requirements specification level) have been checked. In this paper, we propose the use of task structures for modeling user requirements and domain knowledge at the requirements specification level, and the use of high-level Petri nets for expressing and verifying the task structure-based specifications. Issues in mapping task structures onto high-level Petri nets are identified, e.g. the representation of task decomposition, constraints and the state model; the distinction between the "follow" and "immediately follow" operators; and the "composition" operator in task structures. The verification of task structures using high-level Petri nets is performed on model specifications of a task through constraint satisfaction and relaxation techniques, and on process specifications of the task based on the reachability property and the notion of specificity     

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.     

Verifying soundness of business processes: A decision process Petri nets approach

This paper presents a trajectory-tracking approach for verifying soundness of workflow/Petri nets represented by a decision-process Petri net. Well-formed business processes correspond to sound workflow nets. The advantage of this approach is its ability to represent the dynamic behavior of the business process. We show that the problem of finding an optimum trajectory for validation of well-formed business processes is solvable. To prove our statement we use the Lyapunov stability theory to tackle the soundness verification problem for decision-process Petri nets. As a result, applying Lyapunov theory, the well-formed verification (soundness) property is solved showing that the workflow net representation using decision process Petri nets is uniformly practically stable. It is important to note that in a complexity-theoretic sense checking the soundness property is computationally tractable, we calculate the computational complexity for solving the problem. We show the connection between workflow nets and partially ordered decision-process Petri net used for business process representation and analysis. Our computational experiment of supply chains demonstrate the viability of the modeling and solution approaches for solving computer science problems.     

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.     

Soundness-preserving reduction rules for reset workflow nets

The application of reduction rules to any Petri net may assist in its analysis as its reduced version may be significantly smaller while still retaining the original net’s essential properties. Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove all tokens from a certain place. Such nets have a natural application in business process modelling where possible cancellation of activities need to be modelled explicitly and in workflow management where such process models with cancellation behaviours should be enacted correctly. As cancelling the entire workflow or even cancelling certain activities in a workflow has serious implications during execution (for instance, a workflow can deadlock because of cancellation), such workflows should be thoroughly tested before deployment. However, verification of large workflows with cancellation behaviour is time consuming and can become intractable due to the state space explosion problem. One way of speeding up verification of workflows based on reset nets is to apply reduction rules. Even though reduction rules exist for Petri nets and some of its subclasses and extensions, there are no documented reduction rules for reset nets. This paper systematically presents such reduction rules. Because we want to apply the results to the workflow domain, this paper focusses on reset workflow nets (RWF-nets), i.e. a subclass tailored to the modelling of workflows. The approach has been implemented in the context of the workflow system YAWL.     

Virtual prototyping of automated manufacturing systems with Geometry-driven Petri nets

The design process of automated manufacturing systems typically involves physical prototypes to validate the interactions between hardware and software components. However, physical prototyping is expensive and time consuming, which often leads to insufficient opportunities for testing early during the development cycle. Our objective is to improve this situation by providing a method to develop realistic prototypes using virtual reality technology that can be applied during earlier development stages. Our approach combines a virtual reality engine capable of enacting the laws of rigid body physics with a new hybrid software modelling language to control the simulated hardware using virtual sensors and actuators as they would be present in a physical prototype. The new modelling language is called Geometry-driven Petri nets (GPN) and combines a class of timed, high-level Petri nets with data structures used in state-of-the-art VR environments. This article describes the new GPN approach, applies it to a case study of an automated manufacturing line, and compares it with related approaches.     

A compositional Petri net translation of general π-calculus terms

We propose a finite structural translation of possibly recursive π-calculus terms into Petri nets. This is achieved by using high-level nets together with an equivalence on markings in order to model entering into recursive calls, which do not need to be guarded. We view a computing system as consisting of a main program (π-calculus term) together with procedure declarations (recursive definitions of π-calculus identifiers). The control structure of these components is represented using disjoint high-level Petri nets, one for the main program and one for each of the procedure declarations. The program is executed once, while each procedure can be invoked several times (even concurrently), each such invocation being uniquely identified by structured tokens which correspond to the sequence of recursive calls along the execution path leading to that invocation.