Post and pre-initialized stopwatch Petri nets: Formal semantics and state space computation

Adib Allahham*, Hassane Alla

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


A modeling paradigm is introduced which defines an extension of T-Time Petri Nets with the concept of Stopwatch. In this model, stopwatches which are associated with transitions, can be reset either by using classical mechanism in Time Petri Nets or by the firing of the corresponding transitions. The resulting model, which we call Post- and Pre-initialized Stopwatch Petri Nets or SWPN, permits a natural description of so-called preemption-resume behavior. We give the formal semantics of this model as a timed transitions system and we position SWPN with regard to other classes of Petri nets destined to model preemptive behavior. We also propose a method for computing the state space of a SWPN as a stopwatch automaton. The method consists of labeling firstly the marking graph of a SWPN as a stopwatch automaton. Then, a forward region-based algorithm is applied to this automaton by using an analyzing tool on linear hybrid system PHAVer in order to compute its reachable states. The obtained automaton is proved to be timed bisimilar to initial SWPN. Thus, the verification of quantitative properties can be conducted thanks to the such obtained automaton.

Original languageEnglish
Pages (from-to)1175-1186
Number of pages12
JournalNonlinear Analysis: Hybrid Systems
Issue number4
Publication statusPublished - Nov 2008
Externally publishedYes

Cite this