Article Preview
TopIntroduction
Petri Nets are a well-established formal model for the specification of distributed and concurrent systems. This model is very attractive by its ability to capture causal and parallel behaviours of these systems. Since its introduction, timed models based on Petri Nets have been extensively studied for the specification and verification of real-time systems.
The two main extensions of Petri Nets with time are Timed Petri Nets (TdPN) and Time Petri Nets (TPN) (Ramchandani, 1974;Merlin, 1974). In TdPNs, delays were first associated with transitions (T-TdPN) and then to places (P-TdPN) (Ramchandani, 1974; Sifakis, 1977). The two corresponding subclasses namely T-TdPN and P-TdPN are expressively equivalent (Ramchandani, 1974; Sifakis, 1977) and are a subclass of TPNs. Thus, a time delay can represent a minimum duration of firing or a minimum residence time of a token in a place. Informally, the TdPN uses the notion of duration as opposed to the notion of period of TPN.
In TPNs, temporal extension is expressed as an interval associated mainly to transitions (T-TPNs), to places (P-TPNs) or arcs (A-TPNs) (Merlin, 1974; Khansa, 1997; Walter, 1983). Regarding the expressiveness of T-TPN and P-TPN, Khansa et al. (1996) showed that these two models are incomparable. A-TPNs and P-TPNs are similar; however, the only difference concerns the strong semantics of P-TPNs and the lazy semantics of A-TPNs (Boyer, 1997). At last, T-TPNs form a subclass of Time Stream Petri Nets (Emerson, 1990) that have been introduced to model multimedia applications.
TPNs are primarily used for performance analysis. In these models the firing of transitions is of null duration. They natively express specifications in time. In explaining beginnings and ends of actions with specification of time progress, they can also express specifications in duration. However, this manner of modelling the action durations has many disadvantages. First, the size of the associated semantic structure is increased. This phenomenon is known as the state space combinatorial explosion problem. Second, the obtained specification structurally keeps out the statement of system to be specified. Third, the underlying semantics, usually the interleaving semantics, supposes structural and temporal atomicity of actions, i.e., actions are indivisible and have null duration. Moreover, this semantics gives abstracts to the parallel execution of actions.
With the assumption that the firing of each transition corresponds to the execution of a divisible action with duration, our goal is to exploit a model which permits expressing true-concurrency in a natural way without splitting actions into their start and end events. To do this, we propose at first an extension of TPN model called Time Petri Nets with Duration Action (DTPN). In this model, two annotations are associated to each transition, namely its timing constraint that restricts the date at which it can be fired and the duration of its corresponding action. Consequently, DTPNs can be considered as a generalization of Merlin’s TPNs, T-TdPNs and P-TdPN (Merlin, 1974; Ramchandani, 1974; Sifakis, 1977). Then, we give true-concurrency semantics to DTPN in terms of maximality semantics (Devillers, 1992; Courtiat & Saїdouni, 1995; Saїdouni & Courtiat, 2003; Saїdouni Belala & Bouneb, 2008; Saїdouni, Belala & Bouneb, 2009). This semantics has been proven necessary and sufficient for the action refinement and for action durations (Saїdouni, 1996). The underlying model is a Durational Action Timed Automaton (DATA) (Saїdouni & Belala, 2006).