Solving the Problem of Forbidden States in Discrete Event Systems: A Novel Systematic Method for Reducing the Number of Control Places

This paper deals with the problem of forbidden states in Discrete Event Systems modelled by non‐safe Petri Nets. To avoid these states, some Generalized Mutual Exclusion Constraints can be assigned to them. These constraints limit the weight sum of tokens in some places and can be enforced on the system using control places. When the number of these constraints is large, a large number of control places should be added to the system. In this paper, a method is presented to assign the small number of constraints to forbidden states using some states which cover the forbidden states. So, a small number of control places are added to the system leading to obtaining a maximally permissive controller.     

延迟时间Petri网的验证分析

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

模糊Petri网的反馈控制研究

本文首先将模拟技术应用于Ｐｅｔｒｉ网中，得到模糊Ｐｅｔｒｉ网模型，然后基于Ｐｅｔｒｉ网中的库所湾量的概念，在普通Ｐｅｔｒｉ网的反馈控制基础上提出了一种模型Ｐｅｔｒｉ网的反馈控制方法。该方法使得对复杂系统的模糊Ｐｅｔｒｉ多控制器的系统设计成为可能。     

Controller Synthesis with Highly Simplified Linear Constraints

This paper deals with the problem of forbidden states in safe Petri nets to obtain a maximally permissive controller. To prevent the system from entering the forbidden states, assigning some constraints to them is possible. The constraints can be enforced on the system using control places. When the number of forbidden states is large, a large number of constraints should be assigned to them. This results in a large number of control places being added to the model of the system, which causes a complicated model. Some methods have been proposed to reduce the number of constraints. Nevertheless, they do not always give the best results. In this paper, two ideas are offered to reduce the number of constraints, giving a more simplified controller.     

Computer aided verification of Lamport's fast mutual exclusionalgorithm using colored Petri nets and occurrence graphs with symmetries

In this paper, we present a computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Colored Petri Nets (CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a significant increase in the number of states which can be analyzed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. CP-nets and OS-graphs are not our invention. Our contribution is the development of the tool and verification of the example, demonstrating how the method of occurrence graphs with symmetries can be put into practice     

Graphical simulation of Petri Nets

An interactive graphics package for modeling with Petri Nets has been implemented. It uses the VT-11 graphics terminal supported on the PDP-11/35 computer to draw, execute, analyze, edit and redraw a Petri Net. Each of the above mentioned tasks can be performed by selecting appropriate items from a menu displayed on the screen. Petri Nets with a reasonably large number of nodes can be created and analyzed using this package. The number of nodes supported may be increased by making simple changes in the program. Being interactive, the program seeks information from the user after displaying appropriate messages on the terminal. After completing the Petri Net, it may be executed step by step and the changes in the number of tokens may be observed on the screen, at each place. Some properties of Petri Nets like safety, boundedness, conservation and redundancy can be checked using this package. This package can be used very effectively for modeling asynchronous (concurrent) systems with Petri Nets and simulating the model by “graphical execution.”     

Covering sharing trees: a compact data structure for parameterized verification

The control state reachability problem is decidable for well-structured infinite-state systems like (Lossy) Petri Nets, Vector Addition Systems, and broadcast protocols. An abstract algorithm that solves the problem is the backward reachability algorithm of [1, 21 ]. The algorithm computes the closure of the predecessor operator with respect to a given upward-closed set of target states. When applied to this class of verification problems, symbolic model checkers based on constraints like [7, 26 ] suffer from the state explosion problem.In order to tackle this problem, in [13] we introduced a new data structure, called covering sharing trees, to represent in a compact way collections of infinite sets of system configurations. In this paper, we will study the theoretical complexity of the operations over covering sharing trees needed in symbolic model checking. We will also discuss several optimizations that can be used when dealing with Petri Nets. Among them, in [14] we introduced a new heuristic rule based on structural properties of Petri Nets that can be used to efficiently prune the search during symbolic backward exploration. The combination of these techniques allowed us to turn the abstract algorithm of [1, 21 ] into a practical method. We have evaluated the method on several finite-state and infinite-state examples taken from the literature [2, 18 , 20 , 30 ]. In this paper, we will compare the results we obtained in our experiments with those obtained using other finite and infinite-state verification tools.     

基于Petri网与SimEvents的半导体晶圆生产线建模与仿真

SimEvents与Petri网相结合是一种很好的复杂生产线建模仿真方法,应用这一方法建立了一条300mm晶圆生产线的仿真模型.描述了其Petri网模型建立的总体流程和各个详细步骤,以及在SimEvents环境下实现Petri网模型并进行仿真的关键技术.在此基础上,对晶圆生产的不同调度方案分别进行了仿真,并把仿真结果进行了比较,从而验证了仿真建模方法的正确性.     

An Assertional Language for the Verification of Systems Parametric in Several Dimensions: (Preliminary Results)

We propose a rich assertional language to be used for symbolic verification of systems with several parametric dimensions. Our approach combines notions coming from different fields. We use Colored Petri Nets [16] to describe nets of processes carrying structured data. We combine concepts coming from constraint programming [23] and multiset rewriting [19] to finitely and concisely represent transitions and infinite collection of states of Colored Petri Nets. Finally, we incorporate these concepts in the verification technique based on backward reachability and upward-closed sets of [1,12]. We obtain a procedure that can be used as an automatic support for attacking parameterized verification problems. We apply these ideas to verify safety properties of a parameterized mutual exclusion algorithm. A number of open questions arise from our preliminary experiments, finding an adequate counterpart of our framework in the world of automated deduction being among the more interesting ones.     

A methodology to specify three-dimensional interaction using Petri Nets

This work presents a methodology to formally model and to build three-dimensional interaction tasks in virtual environments using three different tools: Petri Nets, the Interaction Technique Decomposition taxonomy, and Object-Oriented techniques. User operations in the virtual environment are represented as Petri Net nodes; these nodes, when linked, represent the interaction process stages. In our methodology, places represent all the states an application can reach, transitions define the conditions to start an action, and tokens embody the data manipulated by the application. As a result of this modeling process we automatically generate the core of the application's source code. We also use a Petri Net execution library to run the application code. In order to facilitate the application modeling, we have adapted Dia, a well-known graphical diagram editor, to support Petri Nets creation and code generation. The integration of these approaches results in a modular application, based on Petri Nets formalism that allows for the specification of an interaction task and for the reuse of developed blocks in new virtual environment projects.     

Petri网及其扩展研究

Petri网是一种应用非常广泛的建模工具。首先给出了基本Petri网的概念,在此基础上对多种Petri网进行了广泛的研究,包括时间因素Petri网、有色Petri网、面向对象Petri网、模糊Petri网及受控Petri网,并针对每种Petri网的特点和应用范围进行了讨论,提出了Petri网当前发展的方向和急需解决的热点问题。     

一种生成具有变量标识的高级Petri网可达树的算法

Petri网动态性质的考察一般基于网不变量(Net Invariants)和可达树(Reachability Tree).这两个概念已被扩展到高级Petri网中.高级Petri网可达集空间随着网的复杂性而指数性增长是计算可达树问题中的一个主要难 点.本文定义了具有变量标识的高级Petri网并给出了构造该类网的可达树的算法.本文的算法以变量标识的等价关系(equivalent relation)和覆盖关系(covering relation)为基础,明显地简化了可达集空间.个体标识的信息可从变量标识的定义域中获得.     

Petri网在C3I系统仿真建模中的应用

建模仿真技术是C^3I系统性能评估、C^3I系统仿真分析与设计的一个重要方法。该文介绍了Petri网的基本概念,说明了Petri网建模的特征;给出了一种应用于C^3I系统仿真研究的建模方法：应用Petri网对C^3I系统进行分析与设计,实现从C^3I系统的组织框图到Petri网数学模型的转换;指出了Petrl网在C^3I系统仿真建模方面的不足和改进方向。最后,该文给出了用Petri网建模的一个简单应用实例。     

一类DEDS状态反馈控制器综合的新方法

对具有无穷状态空间的并发离散事件动态系统提出了一种基于Petri网图示的矩阵代数 综合方法.该方法借助于对Petri网的结构分解可以用于结构无竞争Petri网描述的一类离 散事件动态系统状态反馈控制器的离线综合.     

An SPN-Neural Planning Methodology for Coordination of two Robotic Hands with Constrained Placement

This paper presents a planning methodology based on Stochastic Petri Nets (SPNs) and Neural nets for coordination of two robotic arms working in a space with constrained placement. The SPN planning method generates a global plan based on the states of the elements of the Universe of Discourse. The plan includes all the possible conflict-free planning paths to achieve the goals under constraints, such as specific locations on which objects have to be placed, order of placement, etc. An associated neural network is used to search the vectors of markings generated by the SPN reachability graph for the appropriate selection of plans. Moreover, it preserves all the interesting features of the SPN model, such as synchronization, parallelism, concurrency and timing of events. The coordination of two robotic arms is used as an illustrative example for the proposed planning method, in a UD space where the location of objects placement are restricted.     

基于Petri网的联锁软件安全性测试的研究

安全是铁路运输生产永恒的主题。联锁软件是保障铁路车站列车或机车(以下简称列机车)作业安全的关键软件,充分的测试对于保证其安全性具有举足轻重的作用。文章在分析文献[1][5][6]的联锁软件安全性需求故障树模型的基础上建立了联锁软件安全性需求的Petri网模型,提出了一种基于十字链表的Petri网的存储结构,给出了一种求解割集的算法实现;接着简述了安全性测试用例的自动生成方法;最后给出了该方法在HJ04A系统联锁软件安全性测试中的应用。     

时间约束工作流的可调度性分析

提出一种时间约束工作流的可调度性分析方法。针对时间约束Petri网（Timing Constraint Petri Nets,TCPN）为普通Petri网无法建模多参与资源的不足,给出了扩展的时间约束Petri网（w-TCPN）的定义;结合w-TCPN的拓扑结构,从模型和实例两个层次,给出了w-TCPN变迁可调度的判定定理;提出了时间约束的调整策略。w-TCPN的研究使得时间约束工作流的建模和可调度性分析更加合理。     

Implementing Coloured Petri Nets Using a Functional Programming Language

Coloured Petri Nets (CPNs) are a graphically oriented modelling language for concurrent systems based on Petri Nets and the functional programming language Standard ML. Petri Nets provide the primitives for modelling concurrency and synchronisation. Standard ML provides the primitives for modelling data manipulation and for creating compact and parameterisable CPN models.Functional programming and Standard ML have played a major role in the development of CPNs and the CPN computer tools supporting modelling, simulation, verification, and performance analysis of concurrent systems. At the modelling language level, Standard ML has extended Petri Nets with the practical expressiveness required for modelling systems of the size and complexity found in typical industrial projects. At the implementation level, Standard ML has been used to implement the formal semantics of CPNs that provide the theoretical foundation of the CPN computer tools.This paper provides an overview of how functional programming and Standard ML are applied in the CPN modelling language and the supporting computer tools. We give a detailed presentation of the key algorithms and techniques used for implementing the formal semantics of CPNs, and we survey a number of case studies where CPNs have been used for the design and analysis of systems. We also demonstrate how the use of a Standard ML programming environment has allowed Petri Nets to be used for the implementation of systems.     

基于Stateflow的Petri网仿真方法

Stateflow是matlab环境下与simulink整合在一起的专门用来对复杂响应系统和事件驱动系统进行仿真的工具箱。应用其对Petri网模型进行仿真,提出了一种对Petri中资源的分类方法,根据petri网中资源的流通方式将资源分为循环资源、非循环资源．及隐性资源。并结合变迁的个数和激活方式给出了从一个已知的Petri网构造其相应的Stateflow的具体规则．及详细步骤,最后结合某汽车冲压单元的建模进行举例说明。构造过程显示出文中提出的仿真方法具有使用简单、通用性强、扩展性好的特点。