From Time Petri Nets to Timed Automata
Franck Cassez, H Roux Olivier · 2008
In this chapter we introduce a formalism, Time Petri Nets (TPNs), to model real-time systems.We compare it with another well-known formalism, Timed Automata (TA), used for specifying timed systems.We precisely define the semantics of TPNs and TA and compare them according to two criteria: the languages (or set of behaviours) they can generate, and the trees (or branching behaviours) they can generate.We show that every TPN can be translated into an equivalent 1 TA.Then, we introduce a real-time logic to specify properties of real-time systems.We show how to check that a given TPN satisfies a property written in this logic.For this, we use our translation 2 from TPNs to TA and check the property on the equivalent TA.Finally we briefly report on experiments for checking real-time properties of TPNs using this framework. Petri Nets with TimeThe two main extensions of Petri Nets with time are Time Petri Nets (TPNs) (Merlin, 1974) and Timed Petri Nets (Ramchandani, 1974).In a TPN a transition can fire within a time interval whereas for Timed Petri Nets it fires as soon as possible.For Timed Petri Nets, time can be considered relative to places or transitions (Sifakis, 1980;Pezzè, 1999).It is interesting to formally compare the different classes of Petri Nets with time: this gives a better idea of what one subclass should be used for.The expressive power of (time) Petri Nets can be compared w.r.t. the set of (timed) behaviors they can generate.One class C is a subclass of another C ′ , if for every net n in C, there is a net n ′ in C ′ which can generate the same behaviors as n.In this case, we say that the class C is less expressive than C ′ .For instance, the two subclasses P-Timed Petri Nets and T-Timed Petri Nets are expressively equivalent (Sifakis, 1980;Pezzè, 1999) (i.e., P-Timed Petri Nets are less expressive than T-Timed Petri Nets and vice-versa).The same subclasses are defined for TPNs i.e., T-TPNs and P-TPNs.Both classes of Timed Petri Nets are less expressive than both P-TPNs and T-TPNs (Pezzè, 1999).P-TPNs and T-TPNs are incomparable (Khansa et al., 1996).Finally TPNs are less expressive than Time Stream Petri Nets (Diaz and Senac, 1994) which were introduced to model multimedia applications.Another way of comparing two classes is to determine the status of different decision problems (e.g., reachability, coverability, boundedness) for the two classes.For instance, reachability is undecidable for TPNs, as well as boundedness.Recent work (de Frutos Escrig et al., 2000;Abdulla and Nylén, 2001) considers timed arc Petri nets where each token has a clock representing its "age".The authors prove that coverability and boundedness are decidable for this class of Petri nets by applying a backward exploration technique.They use a lazy (nonurgent) behavior of the net: the firing of transitions may be delayed, even if that implies that 1 This equivalence is formally defined in the chapter. 2 This translation preserves the properties of this logic.