A generalized Petri net modeling approach for the control of re-entrant flow semiconductor wafer fabrication

Re-entrant flow manufacturing lines, such as occur in semiconductor wafer fabrication, are characterized by a product routing that consists of multiple visits to a workstation or group of workstations during the manufacturing process. In this paper, a modeling approach is based on the use of generalized Petri nets for a re-entrant flow manufacturing line is presented. Specifically, three Petri net models representing a re-entrant flow line with three work centers and six machines are modeled. How these models may be used to represent a variety of queuing disciplines and work release policies is discussed.     

一种不确定时段的扩展时段对序逻辑：时间Petri网模型表示和线性推理

针对点－时段时序逻辑的不足,提出了一种新的时段时序逻辑－－扩展时段时序逻辑,对不确定时间段发生的事件具有较好的描述能力。时间Petri网模型表示的引入,增强了扩展时段时序逻辑的描述直观性及分析能力,为进行线性推理提供了有利的工具。同时还提出了几种变迁间的实施推理规则。运用这些规则可以简化复杂时序关系的Petri网模型,并在线性时间复杂度内定量地得到各变迁间的时序逻辑关系,因而是一种行这有效的方法。     

Automatic Real-Time Analysis of Reactive Systems with the PARTS Toolset

Real-time systems are becoming increasingly widespread, often in safety-critical applications. It is therefore crucial that these systems be correct; however, there are few automated tools for analyzing concurrency and timing properties of these systems. The PARTS toolset uses a Petri-net-based reachability analysis to analyze program specifications written in an Ada-83 subset. Our simple time Petri nets are specifically aimed at facilitating real-time analysis. In order to control the state-explosion problem, PARTS employs several optimization techniques aimed at state-space reduction. In this paper we discuss our approach and we report on extensive experiments with several examples of real-time specifications based on Ada 83. When possible, we also compare our experimental results with results obtained by other approaches to real-time analysis.     

A multi-agent intelligent system for efficient ERP maintenance

The Enterprise Resource Planning (ERP) system is an enterprise-wide integrated software package designed to uphold the highest quality standards of business process. However, for the time being, when the business condition has been changed, the system may not guarantee that the process embedded in ERP is still best. Moreover, since the ERP system is very complex, maintaining the system by trial and error is very costly. Hence, this paper aims to construct a support system that adjusts ERP system to environmental changes. To do so, we adopt multi-agent intelligent technology that enables autonomous cooperation with one another to monitor ERP databases and to find any exceptional changes and then analyze how the changes will affect ERP performance. Moreover, Petri net is applied to manage the complexity and dynamics of agents’ behavior. To show the feasibility of the idea, a prototype agent system, ERP/PN, is proposed and an experiment is conducted.     

客户机／服务器系统缓冲区容量的Petri网分析

本文在详细分析客户机／服务器架构的基础上,采用随机Petri网方法对客户机／服务器体系进行建模,着重就模型的缓冲区性能给出了相应的GSPN性能计算方法,并结合实例进行定性分析。     

过程建模的Petri网模型

工作流管理的问题由于广泛存在于计算机应用的许多方面而迅速得到发展。本文介绍了一个以扩展的Petri网作为建模工具、以消息队列作为执行机制实现的过程管理的原型系统。该模型描述了活动的并发执行和依赖关系、活动激发的条件、事件顺序及文档管理等信息。执行该模型,在分布、异构、自治的环境中可自动监视、管理和调度工作任务,为业务过程重组、业务过程自动化提供了有力的支持。     

电力系统结线分析的有色Petri网方法

从离散事件动态系统角度考虑电力系统结线分析问题,提出了基本分析单元的有色Petri网模型以及基于该Petri网的结线分析算法,Petri网中的令牌代表结线分析中的结点,令牌的颜色表示连接在同一个结点上的元件,变迁将包含相同元件的结点连接在一起,论文对基于Petri网的结线分析算法及传统的算法进行了比较,并计算了一个模型系统各变电站的结点及网络的结线,表明了该方法的可行性及有效性。     

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.

ReSpecT Nets: Towards an Analysis Methodology for ReSpecT Specifications

A key feature for infrastructures providing coordination services is the ability to define the behaviour of coordination abstractions according to the requirements identified at design-time. We take as a representative for this scenario the logic-based language ReSpecT (Reaction Specification Tuples), used to program the reactive behaviour of tuple centres. ReSpecT specifications are at the core of the engineering methodology underlying the TuCSoN infrastructure, and are therefore the “conceptual place” where formal methods can be fruitfully applied to guarantee relevant system properties.In this paper we introduce ReSpecT nets, a formalism that can be used to describe reactive behaviours that can succeed and fail, and that allows for an encoding to Petri nets with inhibitor arcs. ReSpecT nets are introduced to give a core model to a fragment of the ReSpecT language, and to pave the way for devising an analysis methodology including formal verification of safety and liveness properties. In particular, we provide a semantics to ReSpecT specifications through a mapping to ReSpecT nets. The potential of this approach for the analysis of ReSpecT specifications is discussed, presenting initial results for the analysis of safety properties.