Petri网化简操作及其在系统验证中的应用

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

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

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

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

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

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

针对企业用加工厂或车间加工某种产品等这一类业务处理问题，提出了用Petri网精细化操作解决问题的方案。定义了一种TT-型子网，用这种子网分别对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网和状态方程模型

柔性制造系统(FMS)的实时调度问题是一个典型的并发系统(CA),亦称为离散事件动态系统(DEDS).这是一类很复杂的动态系统,本文尝试用Petri网和有色Petri网对FMS的实时调度问题建立动态模型并同时给出了代数形式的状态方程模型.     

Petri网共享PP-型子网合成性质分析

Petri网合成可以避免状态空间按指数阶迅速扩大的问题,并且在网扩大时可以保持原网的某些优良性质.为了解决资源共享问题,焦莉等人对于一个满足死锁-陷阱性质(ST-property)的非对称选择网(asymmetric choice,简称AC)进行库所合并,给出了合并后的网保持原网活性、有界性和可回复性的条件.主要动机是对焦莉等人的研究结果进行推广,把对于AC网的库所合并问题推广到AC网或更一般的Petri网上的子网共享合成问题.给出了使共享PP-型子网合成Petri网系统保持活性、有界性和可回复性的条件以及多个AC网进行共享PP-型子网合成,使得到的合成网仍为AC网的条件.结果可为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网系统合成性质的考察提供有效途径，为复杂大系统的分析提供重要手段，并特别适合于一类系统的设计和分析，具有一定的实用价值。     

Preserving Languages and Properties in Stepwise Refinement-Based Synthesis of Petri Nets

The current stepwise refinement operation of Petri nets mainly concentrates on property preservation, which is an effective way to analyze and verify complex systems. Further steps into this field are needed from the perspective of system synthesis and language preservation. First, the refinement of Petri nets is introduced based on a k-well-behaved Petri net, in which k tokens can be processed. Then, according to the different compositions of subsystems, well-, under- and overmatched refined Petri nets are proposed. In addition, the language and property relationships among sub-, original, and refined nets are studied to demonstrate behavior characteristics and property preservation in a system synthesis process. A manufacturing system is given as an example to illustrate the effectiveness of the proposed approach in synthesizing and analyzing the Petri nets of complex systems.     

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网方法及其在软件工程中的应用

本文介绍了面向对象Ｐｅｔｒｉ网方法，给出了ＯＯＰＮ的基本定义和图形表示，讨论了ＯＯＰＮ的特性和子网细化方法。     

Modeling of reconfigurable manufacturing systems based on colored timed object-oriented Petri nets

To cope with the rapid change in manufacturing market requirements, reconfigurable manufacturing systems (RMSs) with the feature of reconfigurability, have to be developed. A model that describes the reconfiguring process of a manufacturing system is developed by applying colored timed object-oriented Petri nets. Based on the main difference between configurations of RMSs and flexible manufacturing systems (FMSs), a modular hierarchical structure of RMS is developed. By the object-oriented method, all the object classes in the RMS model are identified. A macro-place is used to model the aggregation of many processes and a macro-transition is used to link all the related macro-places. Macro-places and macro-transitions are connected with arcs to form a Petri net named a macro-level Petri net so that the control logic of RMS is represented. The macro-level Petri net is refined by hierarchical steps, each step describing these macro-places by more detailed sub macro-places until all the macro-places cannot be divided. Then the characteristics of material flow and time constraints in RMS are modeled by applying colored tokens and associated time-delay attributes. This model integrates object-oriented methods, stepwise refinement ideas and Petri nets together. The RMS activities can be encapsulated and modularized by the proposed method, so that RMS can be easily constructed and investigated by the system developers.