On Time Invariance in Time Petri Nets

Louchka Popova-Zeugmann

Humboldt-Universität zu Berlin, Institut für Informatik PF 1297, D-10099 Berlin, e-mail: popova@informatik.hu-berlin.de

Extended abstract

Clasical Petri Nets are a well known formalism for describing and analysing different systems, especially for parallel and concurent systems. Almost, the clasical Petri Nets are not sufficient for studying some special properties as random properties, time dependances, unfinite domains etc.

Certain local time dependances between some processes/actions in a parallel or concurent system are often given resp. claimed. For studying such systems a large variety of time dependent Petri Nets are defined and well searched and meanwhile widely applicated.

All these nets have the same origin: the classical Petri Nets. Then, in different ways the time is associated. In this lecture we are dealing with Time Petri Nets, introduced 1972 by Merlin and further investigated by Berthomieu/Menasche[3], Popova[6],[7], Berthomieu/Diaz[2], Boucheneb/Berthelot[4], Berthelot/ Boucheneb[1] etc.

Time Petri Nets are classical Petri Nets where to each transition t a time interval [a_{t}, b_{t}] is associated. The times a_{t} and b_{t} are relative to the moment at which t was last enabled. Assuming that t was last enabled at time c_{t}, then t may fire only during the interval [c_{t} +a_{t}, c_{t} +b_{t}] and must fire at the time c_{t} +b_{t} at the latest, unless it is disabled before by the firing of another transition. Firing a transition takes no time. The Time Petri Nets are well applicable e.g. for design and analysing of communication protocols and further problems with recoverability aspects.

For analysing Time Petri Nets there are defined two different methods: one is defined by Berthomieu/Diaz/Menasche and the other is defined by Popova. The both consist on the computation of a reachability graph of the Time Petri Net but they have different backgrounds. By Berthomieu/Diaz/Menasche the notion ”state” is used for describtion (infinitely) many situations of the Time Petri Nets and it is defined by a marking and time intervals for the enabled transitions (comp. Berthomieu/Menasche[3], Berthomieu/Diaz[2]) while in Popova[7] a state is a description for a snapshot of the net. A state here is given by marking and the momentary local time for the enabled transitions and the empty sign for the disabled transitions. Therefore we develop completely different method for building a reachability graph for a Time Petri Net: a node of the Berthomieu/Diaz/Menasche’s reachability graph (a state class (comp. Berthomieu/Menasche[3], Berthomieu/Diaz[2]) ) include an infinite number of possible situations of the Time Petri Net and is given as a solution of a system of inequalities. The nodes of our reachability graph (comp. Popova[7]) are only the ”essential” states, these are the integer-states, where the momentary local time for all enabled transitions are integers. Obviously, this reachability graph includs only a discrete part of all the situations which are possible for a given Time Petri Net. But the knowledge of the net behaviour in the integer-states is sufficient to know the whole behaviour of the net (comp. Popova [7]). The computing of the integer-states is easy. However, the computation of the reachability graph with the both methods is more time and space expensive as the computation of the reachability graph of the resp. classical Petri Net.

In general, there is just no comparison between the liveness behaviour of a given Time Petri Net and the resp. Petri Net without time restrictions.:

In this lecture we will show that each TPN Z, which resp. PN N^{Z} belong to a certain class of EFC PN, has the same liveness behaviour as N^{Z}. Following, for such nets it is sufficient to stady the liveness in the timeless net - computing the reachability graph or using structural methods as invariants etc. (comp. e.g. Desel[5], Starke[8] etc.).

Let Min(p) and Max(p) be the largest elt of all posttransitions of p resp. the smallest lft of all posttransitionen (formal : Min(p) := max{eft(t) | t ∈ pF } and Max(p) := min{lft(t) | t ∈ pF).

Proposition: Let Z = (P, T, F, V, m_{o}, I) be a TPN with

(1) N^{Z} is a EFC net,

(2) N^{Z} is homogeneous,

(3) Min(p) ≤ Max(p) for each place p ∈ P,

(4) ∀t(t ∈ T ∧ eft(t) = lft(t) ⟶ eft(t) = lft(t) ≠ 0. Then it holds: if N^{Z} is live, then Z is live, too.

Ideas of the proof: An enabled transition can lose its ability to fire only when at least a token on an input place is fired by another transition. Because of the both properties of the TPN, EFC and homogeneous, all the enabled transitions with a common place have the same possibility to fire as in the PN during the interval [Min(p), Max(p)]. In this interval (poss., a timepoint only) there are no priorities.

Furthermore, we will show that omiting one of the conditions (1),(2),(3) or (4) the proposition becomes false.

Another looking for net classes which structural or dynamic properties supply indicating the liveness property of a PN to the resp. TPN is very important because of the practical meaning. For these TPN check the liveness is easier as this in general. Furthermore, for computing the reachability graph of a PN there is a large variety of different tools, running on differeft kinds of computers.

Another point here is, the class given above cen be extended: on the one hand structurally - considering clusters, and on the other hand - considering dynamic properties, e.g. global FCC (comp. Starke[8]). A disatvantage by looking for dynamic restricted net class is the check of such properties. The most of them can be found out by computing the reachability graph of the PN.

References:

[1] BERTHELOT, G., BOUCHENEB, H. : ”Occurrence Graph for Interval Timed Colored Nets” . In: Application and Theory of Petri Nets 1994(LNCS):Springer, 1994; pp.79-98.

[2] BERTHOMIEU, B., DIAZ,M.: ”Modeling and Verification of Time Dependent Systems Using Time Petri Nets”. In IEEE Trans. on Software Eng., Vol. 17, No. 3., 1991; pp. 259-273.

[3] BERTHOMIEU, B., MENASCHE, M.: ”An Enumerative Approach for Analyzing Time Petri Nets”. In: Proceedings IFIP 1983; R. E. A. Mason (ed.); North-Holland, 1983; pp. 41-467.

[4] BOUCHENEB, H., BERTHELOT, G.: ” ”Towards a Simplified Building of Time Petri Net Reachability graphs”. In: Proceedings of Petri Nets and Performance Models PNPM93, Toulouse Frace, 1993, IEEE Computer Society Press.

[5] DESEL, J.: ”Struktur und Analyse von Free-Choice-Petrinetzen”. Wiesbaden: Dt. Univ.-Verl., 1992.

[6] POPOVA-Z.,L.: ”Zeit-Petri-Netze”. Diss, HUB,Berlin, 1989.

[7] POPOVA, L.: ”On Time Petri Nets”. In J. Inform. Process. Cybern. EIK 27 (1991) 4, 227-244.

[8] STARKE, P.: ”Analyse von Petri-Netz-Modellen”. Stuttgart: Teubner, 1990.