基于DTPN的时间Petri网的组件级化简规则

时间Petrl网(TPNs)是实时系统时间特性常用的描述和验证的Petri网模型.组件级化简方法是TPN模型常用的分析方法,在保持外部可观察时间特性的前提下,将组件TPN模型化简成一个很简单的TPN模型.然而它却失去了组件内部的性质,如冲突和并发等性质.文中引人延迟时间Petri网(DTPN),通过组件TPN模型向DTPN模型转化,使化简后模型既保持外部可观察时间特性,又保持组件内部的冲突和并发等性质.为了分析化简后的DTPN模型,文中还提出了一种新的DT-PN调度分析方法.最后通过对一个C2系统的组件TPN模型的分析实例,验证该方法的有效性.     

Reachability analysis of real-time systems using time Petri nets

Time Petri nets (TPNs) are a popular Petri net model for specification and verification of real-time systems. A fundamental and most widely applied method for analyzing Petri nets is reachability analysis. The existing technique for reachability analysis of TPNs, however, is not suitable for timing property verification because one cannot derive end-to-end delay in task execution, an important issue for time-critical systems, from the reachability tree constructed using the technique. In this paper, we present a new reachability based analysis technique for TPNs for timing property analysis and verification that effectively addresses the problem. Our technique is based on a concept called clock-stamped state class (CS-class). With the reachability tree generated based on CS-classes, we can directly compute the end-to-end time delay in task execution. Moreover, a CS-class can be uniquely mapped to a traditional state class based on which the conventional reachability tree is constructed. Therefore, our CS-class-based analysis technique is more general than the existing technique. We show how to apply this technique to timing property verification of the TPN model of a command and control (C2) system.     

Discrete Time Stochastic Petri Nets

Basic graph models of processes, such as Petri nets, have usually omitted the concept of time as a parameter. Time has been added to the Petri net model in two ways. The timed Petri net (TPN) uses a fixed number of discrete time intervals. The stochastic Petri net (SPN) uses an exponentially distributed random variable. In this paper, a discrete time stochastic Petri model is described. These discrete time SPN's fill the gap between TPN and normal SPN. However, the use of discrete time complicates the SPN model in that more than one transition may fire at a time step. Finally, an example of a live and bounded Petri net which has nonempty, disjoint, recurrent subsets of markings is given.     

Modeling and Inference of Extended Interval Temporal Logic for Nondeterministic Intervals

Extended interval temporal logic (EITL), an extension of the traditional point-interval temporal logic (PITL), is proposed. In contrast to PITL that represents the dynamic aspects of deterministic intervals, EITL can model and reason about the temporal relations among nondeterministic intervals in discrete-event systems, in which the duration of an event is indeterminate and only the lower bound and upper bound of the ending time can be predicted in advance. Time Petri nets (TPNs) are used for modeling EITL, for they give a straightforward view of temporal relations between the extended intervals and also provide a number of theoretical and practical analysis methods. An inference engine based on the TPN modeling complemented with algebraic inequalities is proposed to construct an analytical representation of the EITL relations and solve qualitative temporal reasoning problems. Linear inference mechanism based on TPN reduction rules is used to infer new temporal relations and handle quantitative temporal reasoning problems with linear time complexity, as our example shows.     

Reduction rules for time Petri nets

The goal of net reduction is to increase the effectiveness of Petri-netbased real-time program analysis. Petri-net-based analysis, like all reachabilitybased methods, suffers from the state explosion problem. Petri net reduction is one key method for combating this problem. In this paper, we extend several rules for the reduction of ordinary Petri nets to work with time Petri nets. We introduce a notion of equivalence among time Petri nets, and prove that our reduction rules yield equivalent nets. This notion of equivalence guarantees that crucial timing and concurrency properties are preserved.     

Reduction rules for time Petri nets

 The goal of net reduction is to increase the effectiveness of Petri-net-based real-time program analysis. Petri-net-based analysis, like all reachability-based methods, suffers from the state explosion problem. Petri net reduction is one key method for combating this problem. In this paper, we extend several rules for the reduction of ordinary Petri nets to work with time Petri nets. We introduce a notion of equivalence among time Petri nets, and prove that our reduction rules yield equivalent nets. This notion of equivalence guarantees that crucial timing and concurrency properties are preserved. Received September 12, 1994/July 4, 1995     

扩展时段时序逻辑的模型、一致性和推理

给出了扩展时段时序逻辑的时间Petri网（TPN）模型构造方法，在构造模型的同时对时序关系进行一致性检验，在模型的基础上提出了一种时序关系推理算法，这种推理算法基于TPN模型的性质及基本不等式规则，可由一组已知的扩展时段时序关系推出一些未知的扩展时段时序关系，这种推广理算法的优势在于利用了TNP模型的分析技术，减小了推理的时间复杂度比单纯利用不等式规则的推理更直观，也更简单，是一种有效的方法，最后，对扩展时段时序逻辑的TPN模型进行了扩充，增强了其模型和分析的能力。     

一种基于知识约简的Petri网模型简化方法

提出一种基于知识约简的Petri网模型简化方法,利用知识约简中的属性约简方法,去除Petri网对应的产生式规则的冗余规则和冗余条件,简化产生式规则得出关键规则。经过知识约简后的规则库转化为Petri网模型,此时的Petri网模型的结点数目减少,因此在一定程度上降低了网系统的复杂程度。简化后的模型保持原有的信息量,而所含的库所、变迁得到了减少,在其基础上进行的知识推理,更加简单和高效。最后通过一个病例实例说明,此方法简单实用,可以有效减少时间和空间复杂度,提高知识搜索和推理效率。     

基于时间Petri网的实时系统低能耗高层综合

以时间Petri网为模型,验证系统功能性和实时性,在此基础上,提出了一种由子任务的能耗变化率驱动的启发式能耗优化算法,并针对一类特殊形式的网模型——可组合时间Petri网,设计了相应的简化算法．实验说明,上述算法时间复杂度低,且优化效果接近最优值,能够为实时系统低能耗高层综合提供有力支持．     

Model Checking of Time Petri Nets Using the State Class Timed Automaton

In this paper, we propose a method for building the state class graph of a bounded time Petri net (TPN) as a timed automaton (TA), which we call the state class timed automaton. We consider bounded TPN, whose underlying net is not necessarily bounded. We prove that our translation preserves the behavioral semantics of the TPN (the initial TPN and the obtained TA are proved timed-bisimilar). It allows us to check real-time properties on TPN by using the state class TA. This can be done efficiently thanks to a reduction of the number of clocks. We have implemented the method, and give some experimental results illustrating the efficiency of the translation algorithm in terms of number of clocks. Using the state class TA, we also give a framework for expressing and efficiently verifying TCTL properties on the initial TPN.     

基于Time Petri Nets的UML时序图分析

引入一种称为Clock的变迁,用来改进TPNs,讨论了如何将时序图转换为基于Clock变迁的TPNs,使这种TPNs能正确反映时序图的流程和时间约束。最后,利用普通Petri网的可达性分析技术对时序图模型进行了分析和验证。     

基于逻辑电路的Petri网化简方法

已有的Petri网化简方法需将网的局部结构与化简规则作逐一的比对,步骤较为繁琐,并且所提供的方法不适合于带抑止弧的网.采用一种与传统方法不同的化简思路,首先将网划分为若干个最大无圈子网,将每个最大无圈子网表达为若干个逻辑式.用逻辑代数来完成逻辑式的化简,最后将其结果还原为Petri网回嵌到原网中,完成整个网的化简.给出了寻找最大无圈子网、最大无圈子网的化简算法以及相关的证明.该方法将化简范围扩展到了带抑止弧的无回路的网或网的局部.     

Soundness-preserving reduction rules for reset workflow nets

The application of reduction rules to any Petri net may assist in its analysis as its reduced version may be significantly smaller while still retaining the original net’s essential properties. Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove all tokens from a certain place. Such nets have a natural application in business process modelling where possible cancellation of activities need to be modelled explicitly and in workflow management where such process models with cancellation behaviours should be enacted correctly. As cancelling the entire workflow or even cancelling certain activities in a workflow has serious implications during execution (for instance, a workflow can deadlock because of cancellation), such workflows should be thoroughly tested before deployment. However, verification of large workflows with cancellation behaviour is time consuming and can become intractable due to the state space explosion problem. One way of speeding up verification of workflows based on reset nets is to apply reduction rules. Even though reduction rules exist for Petri nets and some of its subclasses and extensions, there are no documented reduction rules for reset nets. This paper systematically presents such reduction rules. Because we want to apply the results to the workflow domain, this paper focusses on reset workflow nets (RWF-nets), i.e. a subclass tailored to the modelling of workflows. The approach has been implemented in the context of the workflow system YAWL.     

Mapping PUNITY to UniNet

To solve the problems of the interleaving assumption and the single resource in PUNITY(Petri net and UNITY) and Petri net respectively,this paper proposes a set of mapping rules from PUNITY to uniNet.Based on these rules,problems of one field can be transformed to problems of the other field and powerful tools of Petri net and UNITY can be used.The paper gives a sketch of the mapping rules and applies the rules to an example.Meanwhile ,the mapping rules can help computer to translate PUNITY to UniNet easily.     

Comments on “A Petri net model for temporal knowledgerepresentation and reasoning”

Yao (1994) has presented a unified time Petri net model (TPN) for temporal knowledge representation and reasoning, where the TPN model presented has a good contribution to the aspect of temporal knowledge representation and reasoning. However, there are a number of errors which should be corrected. The purpose of the paper is to identify these errors, and the corrections provided permit the readers who have been confused by the errors to gain a better understanding of the good ideas presented.     

混合语义时间Petri 网模型

提出了时间Petri网的混合语义模型,通过在变迁及其非冲突变迁集的最小上界处设置强制实施点,排除冲突变迁对变迁可实施性的影响,达到既能扩大模型调度范围又可保证任务调度时限性的目的,以解决现有语义模型在调度分析上的缺陷.进一步证明了混合语义模型的图灵等价性及标识可达性问题的不可判定性,然后界定了3种语义模型的时间语言接受能力.最后提出了状态类分析方法,用于模型的可调度性分析和时间计算,并以一个柔性制造系统为例,比较和验证了3种语义模型的调度分析能力.     

Relevant Timed Schedules/Clock Vectors for Constructing Time Petri Net Reachability Graphs

We consider here the time Petri nets (the TPN model) and its state space abstractions. We show that only some timed schedules/clock vectors (one per enabled transition) of the clock/firing domains are relevant to construct reachability graphs for the TPN. Moreover, we prove formally that the resulting graphs are smaller than the TPN reachability graphs proposed in the literature. Furthermore, these results establish a relation between dense time and discrete time analysis of time Petri nets and allow also improving discrete time analysis by considering only some elements of the clock/firing domains.     

Distributed simulation of modular time Petri nets: An approach and a case study exploiting temporal uncertainty

This paper proposes an approach to modular modelling and simulation of complex time-critical systems. The modelling language is represented by Merlin and Farber’s Time Petri Nets (TPNs) augmented with inhibitor arcs and modular constructs borrowed from the Petri Net Markup Language (PNML) interchange format. Analysis techniques depend on Temporal Uncertainty Time Warp (TUTW), a time warp algorithm capable of exploiting temporal uncertainty in general optimistic simulations over a networked context. A key feature of the approach is the fact that TPN models naturally exhibit a certain degree of temporal uncertainty which the TUTW control engine can exploit to achieve good speedup without a loss in the accuracy of the simulation results. The developed TUTW/TPN kernel is demonstrated by modelling and simulation of a real-time system example.A preliminary version of this paper was presented at 38th SCS Annual Simulation Symposium, April 4–6, 2005, San Diego (CA), IEEE Computer Society, pp. 233–240. Franco Cicirelli achieved a PhD in computer science from the University of Calabria (Unical), DEIS—department of electronics informatics and systems science. As a postdoc, he is making research on agent and service paradigms for the development of distributed systems, parallel simulation, Petri nets, distributed measurement systems. He holds a membership with ACM. Angelo Furfaro, PhD, is a computer science assistant professor at Unical, DEIS, teaching object-oriented programming. His research interests are centred on: multi-agent systems, modeling and analysis of time-dependent systems, Petri nets, parallel simulation, verification of real-time systems, distributed measurement systems. He is a member of ACM. Libero Nigro is a full professor of computer science at Unical, DEIS, where he teaches object-oriented programming, software engineering and real-time systems courses. He directs the Software Engineering Laboratory (www.lis.deis.unical.it). His current research interests include: software engineering of time-dependent and distributed systems, real-time systems, Petri nets, modeling and parallel simulation of complex systems, distributed measurement systems. Prof. Nigro is a member of ACM and IEEE.