Petri网精细化操作及其在系统设计中的应用

针对柔性制造系统的设计问题,提出了用Petri网精细化操作解决问题的方案.给出了两种精细化操作.研究了Petri网精细化操作的动态性质保持问题,给出了精细化操作保持活性、有界性、可回复性的充分必要条件;对一个柔性制造系统进行了设计和验证.其结果可为Petri网系统静态和动态性质的考察提供有效途径,为Petri网复杂大系统的分析提供重要手段,并特别适合于柔性制造系统的设计,具有一定的实用价值.     

Petri网共享子网合成及其在系统设计中的应用

针对柔性制造系统的设计和分析，提出了经由Petri网共享子网构成合成网的解决方案；研究了Petri网共享子网合成的动态性质保持问题，给出了合成网保持活性、有界性的一组充分条件；对一个柔性制造系统进行了设计和分析。本文的结果可为Petri网系统静态和动态性质的考察提供有效途径，为Petri网复杂大系统的分析提供重要手段，并特别适合于柔性制造系统的设计，具有一定的实用价值。     

Petri网的TT型子网精细化操作性质分析及其应用

针对企业用加工厂或车间加工某种产品等这一类业务处理问题，提出了用Petri网精细化操作解决问题的方案。定义了一种TT-型子网，用这种子网分别对Petri网系统中的某些变迁进行细化，得到更细致、更精确的Petri网系统。研究了Petri网精细化操作的动态性质保持问题，给出这种精细化操作保持活性、有界性、可回复性和公平性的充要条件；本文的结果可为Petri网系统静态和动态性质的考察提供有效途径，为Petri网复杂大系统的分析提供重要手段，并特别适合于一类业务系统的描述和处理，具有一定的实用价值。     

Petri网的PP型子网精细化操作性质分析及应用

针对工厂用车间中的若干台机器加工某些部件等这一类业务处理问题，提出了用Petri网精细化操作解决问题的方案。定义了一种PP型子网，用这种子网分别对Petri网系统中的某些库所进行细化，得到更细致、更精确的Petri网系统。研究了Petri网精细化操作的动态性质保持问题，给出这种精细化操作保持活性、有界性、可回复性和公平性的充要条件；本文的结果可为Petri网系统静态和动态性质的考察提供有效途径，为Petri网复杂大系统的分析提供重要手段，并特别适合于一类业务系统的描述和处理，具有一定的实用价值。     

基于Petri网化简技术的工作流过程模型结构验证

目前,工作流系统向大型化发展,这使得基于可达图的验证技术在对大型模型进行验证时面临着状态空间爆炸的问题.因此,在过程验证之前,对大型模型进行化简是必要的.文中介绍两种化简规则.这些规则将一个大的Petri网化简为更小的Petri网,同时保持合理性属性,保证化简后的Petfi网和原有的Petri网具有相同的属性.介绍了Petri网、Workflow Petri网和过程合理性定义;讨论了针对Petri网的两种化简技术;提出了工作流过程模型结构合理性验证过程.     

关于Petri网精细化操作及其应用研究

为了解决“顾客投诉”等这一类业务处理问题，提出了用Petri网精细化操作解决问题的方案。定义了一种子网，用这种子网分别对Petri网中的某些变迁进行细化，得到更细致、更精确的Petri网。研究了Petri网精细化操作的性质保持问题，给出了这种精细化操作保持结构有界性、守恒性、可重复性、相容性和活性的充分条件。本文的结果可为复杂大系统的分析提供重要手段，并特别适合于一类业务系统的描述和验证，具有一定的实用价值。     

担保业务管理系统工作流的Petri网建模

应用Petri网建模与工作流技术,构建了担保业务管理系统工作流的Petri网模型,并对一个担保业务管理系统工作流实例,给出了基于Petri网化简分析方法的模型化简与性质验证,表明该模型能够对担保业务管理系统工作流进行有效的分析和验证,从而为担保业务管理系统工作流分析提供了理论基础。     

带抑制弧Petri网的保性变换

Petri 网的保性化简是Petri网分析的一种重要途径。带抑制弧的增广Petri网在计算能力上与图灵机等价。针对带抑制的增广Petri网中串联变迁和串联库所两类情况进行了较深入的分析,在给出了相关化简方法的基础上,证明了通过这些化简规则所得到的网系统与原网在活性、有界性、弱公平性等动态性质上仍保持一致。     

基于精炼操作的Petri网建模及其分析方法

针对复杂系统的Petri网建模及其分析问题,定义了Petri网的精炼操作及其相关的Petri网模型.基于序列投影,建立精炼Petri网与原网、子网间的动态行为关联关系,并分析了该精炼操作的相关动态性质,得到一组性质保持判据.最后,基于该方法实现了一个顺序资源共享系统的应用案例的建模及其分析.所提出的方法不仅为复杂系统的Petri建模提供了新的思路,而且有助于复杂Petri网模型的分析和验证.     

可重写Petri网:位置可重写及性质分析

针对Petri网对动态系统重构形式化描述和建模能力的不足,提出了可重写Petri网和位置可重写Petri网的基本概念.分析了位置可重写Petri网保持有界性、保守性、可重复性及活性等性质.给出了位置可重写Petri网保持活性的一个充要条件.证明了共享合成Petri网是位置可重写Petri网的一个实例,建立了退化的位置可重写Petri网模拟共享合成Petri网的算法.所得结果能够为动态重构系统的Petri网形式化建模提供理论方法,为大规模动态分布式系统的形式化验证提供有效途径.     

Petri网共享T型子网合成公平性分析

共享T-型子网合成是研究复杂Petri网系统性质的一个有效途径.本文研究了共享T-型子网合成对参与合成的各网系统的公平性的继承关系,给出了合成网保持公平性的充分条件.随后给出的有关制造系统设计的举例,说明了该合成方法的有效性.本文的结果可为Petri网系统合成性质的考察提供有效途径.     

Petri网共享T型子网合成结构性质分析及其应用

为了解决系统设计中的子系统共享问题，提出了经由Petri网共享T-型子网构成共享T-型子网合成网的解决方案；研究了共享T-型子网合成网的结构性质，提出了共享T-型子网合成网保持结构有界性、守恒性、可重复性、相容性、P-不变量、T-不变量、公平性和结构活性的充分条件或充要条件；特别在证明结构活性保持性的过程中，体现了Petri网层次化的描述方法。本文的结果可为Petri网系统合成性质的考察提供有效途径，为复杂大系统的分析提供重要手段，并特别适合于一类系统的设计和分析，具有一定的实用价值。     

A Petri net synthesis theory for modeling flexible manufacturingsystems

A theory that synthesizes Petri nets for modeling flexible manufacturing systems is presented. The theory adopts a bottom-up or modular-composition approach to construct net models. Each module is modeled as a resource control net (RCN), which represents a subsystem that controls a resource type in a flexible manufacturing system. Interactions among the modules are described as the common transition and transition subnets. The net obtained by merging the modules with two minimal restrictions is shown to be conservative and thus bounded. An algorithm is developed to detect two sufficient conditions for structural liveness of the net. The algorithm examines only the net's structure and the initial marking, and appears to be more efficient than state enumeration techniques such as the reachability tree method. In this paper, the sufficient conditions for liveness are shown to be related to some structural objects called siphons. To demonstrate the applicability of the theory, a flexible manufacturing system of a moderate size is modeled and analyzed using the proposed theory.     

柔性制造系统的时间Petri网建模与分析

时间Petri网是描述和验证实时系统最常用的形式模型之一。建立基于时间 Petri网的典型柔性制造系统模型,利用状态类分析方法,定量计算所有可行调度及其执行时间,进而获得最优调度,为复杂柔性制造系统的建模与调度提供有效的模型支持。     

Deadlock p revention f or flexible manufacturing system

Deadlock must be prevented via the shop controller during the flexible manufacturing system (FMS) performing. Various models have been tried for the analysis and design of shop controller. Petri net is suitable to describe the dynamic behavior of the discrete event system , such as concurrency , conflict and deadlock , however , the verification of the system behavior needs ructure analysis with complex theoretical proof method. Temporal logic model checking has important advantages over traditional theorem prover. It is fully automatic and can produce possible unter- example which is particularly important in finding subtle error in complex transition systems. In this paper ,a new method for the deadlock prevention based on Petri net and Temporal Logic model checking is presented. The specification in the Temporal Logic is expressed according to some result of structure analysis of the Petri net . The model checking is employed to execute the formal verification ,which will conduct an exhaustive exploration of all possible behaviors. Finally ,an example is presented to demonstrate how the method works.     

Deadlock prevention for flexible manufacturing system

Deadlock must be prevented via the shop controller during the flexible manufacturing system （FMS） performing. Various models have been tried for the analysis and design of shop controller. Petri net is suitable to describe the dynamic behavior of the discrete event system, such as concurrency, conflict and deadlock, however, the verification of the .system behavior needs structure analysis with complex theoretical proof method. Temporal logic model checking has important advantages over traditional theorem prover. It is flatly automatic and can produce possible counter-example which is particularly important in finding subtle error in complex transition systems. In this paper, a new method for the deadlock prevention based on Petri net and Temporal Logic model checking is presented. The specification in the Temporal Logic is expressed according to some result of structure analysis of the Petri net. The model checking is employed to execute the formal verification, which will conduct an exhaustive exploration of all possible behaviors. Finally, an example is presented to demonstrate how the method works.