网上证券交易系统的时序Petri网描述及验证

基于时序Petri网对我国现行网上静态和动态证券交易系统进行了模拟、形式描述及功能正确性验证.应用时序逻辑推理规则,从形式上严格证明了证券交易系统需求规范及其时序Petri网模型动态行为的一致性.结果表明,时序Petri网能够清楚而简单地描述事件间的因果关系和时序关系以及并发系统中某些与时间有关的重要性质,如最终性和公平性.因此,时序Petri网可作为并发系统形式化描述和分析的有力工具.     

Automating the Conversion of Colored Petri Nets with Qualitative Tokens Into Colored Petri Nets with Quantitative Tokens

The authors describe an algorithm for conversion of colored Petri nets with qualitative tokens into a colored Petri net with quantitative tokens preserving boundedness, mutual exclusion, and liveness properties. This conversion allows the invariance method to be applied to colored Petri nets, which uses the Truncated Set of Solutions finding algorithm for Petri net state equations expressed through systems of linear homogenous Diophantine equations. To show the algorithm’s efficiency, it is applied to the colored Petri net that models the operation of a grid system. Equivalence of net models is tested by constructing and analyzing equal finite-state machine.     

CPN tools-assisted simulation and verification of nested Petri nets

Nested Petri nets (NP-nets) is an extension of Petri net formalism within the “nets-within-nets” approach, when tokens in a marking are Petri nets wich have autonomous behavior and synchronize with the system net. The formalism of NP-nets allows modeling multi-level multi-agent systems with dynamic structure in a natural way. Currently there is no tool support for NP-nets simulation and analysis. The paper proposes translation of NP-nets into colored Petri nets and using CPN Tools as a virtual machine for NP-nets modeling, simulation and automatic verification.     

POC net,a subclass of Petri nets,and its application to timed Petri nets

Liveness is one of the most important properties of the Petri net analysis. This property is concerned with a capability for firing of transitions. On the other hand, place-liveness is another notion related to liveness, which is concerned with a capability for having tokens in places. Concerning these liveness and place-liveness problems, this paper suggests a new subclass of Petri net, ‘POC nets’, as a superclass of AC nets and DC nets. For this subclass, the equivalence between liveness and place-liveness is shown and a sufficient condition for liveness for this POC net is derived. Then the results are extended to liveness problem of timed Petri nets which have transitions with finite firing durations and the earliest firing rule. Although liveness of a (non-timed) Petri net is neither necessary nor sufficient condition for liveness of a timed Petri net, it is shown that liveness is preserved if the net has POC structure. Furthermore, it is pointed out that if a POC net satisfies some additional condition, Petri net liveness is equivalent to timed Petri net liveness. Finally, it is shown that liveness of timed POC nets with TC structure and the earliest firing rule is decidable with deterministic polynomial time complexity.     

Framework for modeling and analysis of distributed problem-solving systems

Petri nets have the basic concepts necessary to model distributed systems with asynchronous processes. Petri nets are not directly applicable to certain kinds of systems like distributed intelligent systems (DISs). These are complex systems where multiple intelligent agents cooperate through communication to achieve the solution to a problem. The paper identifies the limitations of ordinary Petri nets for modeling DISs and proposes extensions. The extended Petri net incorporates colored tokens, inhibition arcs, non-primitive places and transitions, multiple copies of tokens and cumulative places. It is called a distributed problem-solving Petri net. The definitions and analysis techniques are given and illustrated by means of an example.     

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

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

Dynamic Transition Refinement

Refinement of Petri nets is well suited for the hierarchical design of system models. It is used to represent a model at different levels of abstraction.Usually, refinement is a static concept. For many scenarios, however, it is desirable to have a more flexible form of refinement. For example in the context of service updates, e.g. version control in distributed systems, a mechanism for dynamic transition refinement is needed.The requirement of dynamic refinement at runtime is quite strong. Since we would like to redefine the system structure by itself, transition refinement cannot be implemented by a model transformation. Instead, an approach is needed which allows for dynamic net structures that can evolve as an effect of transitions firing. In previous work we introduced nets-within-nets as a formalism for the dynamic refinement of tokens. Here we consider an extension of nets-within-nets that uses special net tokens describing the refinement structure of transitions. Using this formalism it is possible to update refinements, introduce alternative refinements, etc. We present some formal properties of the extended formalism and introduce an example implementation for the tool Renew in the context of workflow modeling.     

无冲突Petri网的结构活性判定研究

结构活性作为Petri网的重要结构性质,在Petri网活性判定领域具有较高的研究价值。从Petri网有向回路对结构活性的影响入手,分析与判定无冲突Petri网的结构活性,讨论库所元素及其后置变迁之间是否存在有向回路对Petri网结构活性的影响,研究该类Petri网结构活性判定方法的相关条件与结论,得到无冲突Petri网是满足结构活性的充分必要条件。分析结果表明,该判定方法可在多项式时间内判定无冲突Petri网的结构活性。     

Robustness analysis of Petri nets for assembly/disassembly processes with unreliable resources

In most application of Petri nets, resources are modeled as tokens. Unreliable resources pose challenges as existing Petri net theory is deficient in analyzing the impacts of the perturbation due to resource failures. One strategy to analyze a perturbed system is to study its robustness with respect to uncertainties. In this paper, we study the robustness of a class of controlled Petri nets called controlled assembly/disassembly Petri net (CADPN) for assembly/disassembly processes with unreliable resources. The number of tokens in CADPN is not conservative to capture the effects of resource failures. Based on the CADPN model, we characterize different types of tolerable resource failures allowed for a nominal marking of a live CADPN. We show that liveness of a CADPN can still be preserved under tolerable resource failures.     

Reduction rules for reset/inhibitor nets

Reset/inhibitor nets are Petri nets extended with reset arcs and inhibitor arcs. These extensions can be used to model cancellation and blocking. A reset arc allows a transition to remove all tokens from a certain place when the transition fires. An inhibitor arc can stop a transition from being enabled if the place contains one or more tokens. While reset/inhibitor nets increase the expressive power of Petri nets, they also result in increased complexity of analysis techniques. One way of speeding up Petri net analysis is to apply reduction rules. Unfortunately, many of the rules defined for classical Petri nets do not hold in the presence of reset and/or inhibitor arcs. Moreover, new rules can be added. This is the first paper systematically presenting a comprehensive set of reduction rules for reset/inhibitor nets. These rules are liveness and boundedness preserving and are able to dramatically reduce models and their state spaces. It can be observed that most of the modeling languages used in practice have features related to cancellation and blocking. Therefore, this work is highly relevant for all kinds of application areas where analysis is currently intractable.     

Recursive Nested Petri Nets: Analysis of Semantic Properties and Expessibility

Recursive nested Petri nets may contain marked nets, including their own copies, as their tokens. It is proved that the termination problem is decidable for recursive nested nets with autonomous elements. The expessibility of such nets is compared with other extensions of the Petri net formalism.     

基于SPNAT的维修过程建模与仿真方法研究

Petri网是严格定义的数学对象,直观、形象,且可用于动态的行为分析。通过引进退化令牌对随机Petri网进行理论扩展,提出了一种基于退化令牌的随机Petri网（SPNAT）的维修过程建模与仿真方法。最后通过实例验证了该建模方法的有效性和优越性。     

A fuzzy Petri net-based expert system and its application to damageassessment of bridges

In this paper, a fuzzy Petri net approach to modeling fuzzy rule-based reasoning is proposed to bring together the possibilistic entailment and the fuzzy reasoning to handle uncertain and imprecise information. The three key components in our fuzzy rule-based reasoning-fuzzy propositions, truth-qualified fuzzy rules, and truth-qualified fuzzy facts-can be formulated as fuzzy places, uncertain transitions, and uncertain fuzzy tokens, respectively. Four types of uncertain transitions-inference, aggregation, duplication, and aggregation-duplication transitions-are introduced to fulfil the mechanism of fuzzy rule-based reasoning. A framework of integrated expert systems based on our fuzzy Petri net, called fuzzy Petri net-based expert system (FPNES), is implemented in Java. Major features of FPNES include knowledge representation through the use of hierarchical fuzzy Petri nets, a reasoning mechanism based on fuzzy Petri nets, and transformation of modularized fuzzy rule bases into hierarchical fuzzy Petri nets. An application to the damage assessment of the Da-Shi bridge in Taiwan is used as an illustrative example of FPNES.     

On systematic methods to remove redundant monitors from liveness-enforcing net supervisors

Petri nets based deadlock prevention for flexible manufacturing systems has received much attention over the past decade, primarily due to the seminal work of Ezpeleta et al. in 1995. A Petri net based deadlock prevention mechanism is usually implemented by adding monitors or control places to a plant Petri net model such that liveness can be enforced. The significance of this methodology lies in that both a plant model and its supervisor are in a same formalism-Petri nets. Due to the inherent complexity of Petri nets, in theory, the number of additional monitors that have to been added to achieve liveness-enforcement purpose for an uncontrolled plant model is exponential with respect to the size of the model. This paper first proposes a systematic method to minimize the number of additional monitors in a liveness-enforcing Petri net supervisor such that the resultant net system has the same permissive behavior while liveness can still be preserved. Furthermore, for the liveness-enforcing Petri net supervisors of flexible manufacturing systems, which have some particular property, an algorithm is developed such that more permissive liveness-enforcing Petri net supervisors can be obtained after liveness-restrictive monitor removal. Compared with the existing techniques of eliminating redundant monitors in the literature, the complete state enumeration of a supervisor is avoided, which implies the high computational efficiency of the methods in this paper. Flexible manufacturing examples are used to demonstrate the proposed approaches.     

Timing and liveness in continuous Petri nets

Fluidification constitutes a relaxation technique for studying discrete event systems through fluidified approximated models, thus avoiding the state explosion problem. Moreover, the class of continuous models thus obtained may be interesting in itself. In Petri nets, fluidification leads to the so-called continuous Petri nets, which are technically hybrid models. Under infinite server semantics, timing a continuous Petri net model preserves the liveness property, but the converse is not necessarily true, and if the autonomous net model is not live, the timing may transform it into a live model. In this paper, we investigate the conditions on the firing rates of timed continuous models that make a given continuous system live.     

Model checking multi-level and recursive nets

With the increasing complexity of the problems and systems arising nowadays, the use of multi-level models is becoming more frequent in practice. However, there are still few reports in the literature concerning methods for analyzing such models without flattening the multi-level structure. For instance, several variants of multi-level Petri nets have been applied for modeling interaction protocols and mobility in multi-agent systems and coordination of cross-organizational workflows. But there are few automated tools for analyzing the behavior of these nets. In this paper we explain how to detect faults in models based on a representative class of multi-level nets: the nested Petri nets. We translate a nested net into a verifiable model that preserves its modular structure, a PROMELA program. This allows the use of SPIN model checker to verify properties related to termination, boundedness and reachability.     

Deadlock-Freeness Analysis of Continuous Mono-T-Semiflow Petri Nets

Most verification techniques for highly populated discrete systems suffer from the state explosion problem. The “fluidification” of discrete systems is a classical relaxation technique that aims to avoid the state explosion problem. Continuous Petri nets are the result of fluidifying traditional discrete Petri nets. In continuous Petri nets the firing of a transition is not constrained to the naturals but to the non-negative reals. Unfortunately, some important properties, as liveness, may not be preserved when the discrete net model is fluidified. Therefore, a thorough study of the properties of continuous Petri nets is required. This paper focuses on the study of deadlock-freeness in the framework of mono-T-semiflow continuous Petri nets, i.e., conservative nets with a single repetitive sequence (T-semiflow). The study is developed both on untimed and timed systems. Topological necessary conditions are extracted for this property. Moreover, a bridge relating deadlock-freeness conditions for untimed and timed systems is established.     

一类FMS的最佳活Petri网模型的综合

利用Petri网为一类柔性制造系统建模,并讨论避免系统死锁问题.通过Petri网模 型的结构分析,证明了系统产生死锁的一个充分必要条件.给出了避免死锁的最佳控制器,它 可以通过给系统的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.     

基于变迁指标分解的Petri网性质分析

Petri网的分解技术是复杂网系统分析的一种重要手段,基于变迁指标的分解方法将系统分解为一组T-网。通过获得分解子网的结构性质以及子网与原网间的性质保持关系,得到了判定原网结构性质的一些方法和结论;同时给出了判定原网系统活性的一个条件。所得结果为结构复杂Petri网的性质分析提供了有效的方法。