Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-15T15:22:56.686Z Has data issue: false hasContentIssue false

State space computation and analysis of Time Petri Nets

Published online by Cambridge University Press:  11 May 2006

GUILLAUME GARDEY
Affiliation:
IRCCyN (Institut de Recherche en Communication et Cybernétique de Nantes), UMR CNRS 6597, Université de Nantes, École Centrale de Nantes, École des Mines de Nantes, CNRS, 1, rue de la Noë, B.P. 92101 – 44321 Nantes cedex 3, France (e-mail: guillaume.gardey@irccyn.ec-nantes.fr, olivier-h.roux@irccyn.ec-nantes.fr, olivier.roux@irccyn.ec-nantes.fr)
OLIVIER H. ROUX
Affiliation:
IRCCyN (Institut de Recherche en Communication et Cybernétique de Nantes), UMR CNRS 6597, Université de Nantes, École Centrale de Nantes, École des Mines de Nantes, CNRS, 1, rue de la Noë, B.P. 92101 – 44321 Nantes cedex 3, France (e-mail: guillaume.gardey@irccyn.ec-nantes.fr, olivier-h.roux@irccyn.ec-nantes.fr, olivier.roux@irccyn.ec-nantes.fr)
OLIVIER F. ROUX
Affiliation:
IRCCyN (Institut de Recherche en Communication et Cybernétique de Nantes), UMR CNRS 6597, Université de Nantes, École Centrale de Nantes, École des Mines de Nantes, CNRS, 1, rue de la Noë, B.P. 92101 – 44321 Nantes cedex 3, France (e-mail: guillaume.gardey@irccyn.ec-nantes.fr, olivier-h.roux@irccyn.ec-nantes.fr, olivier.roux@irccyn.ec-nantes.fr)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

The theory of Petri Nets provides a general framework to specify the behaviors of real-time reactive systems and Time Petri Nets were introduced to take also temporal specifications into account. We present in this paper a forward zone-based algorithm to compute the state space of a bounded Time Petri Net: the method is different and more efficient than the classical State Class Graph. We prove the algorithm to be exact with respect to the reachability problem. Furthermore, we propose a translation of the computed state space into a Timed Automaton, proved to be timed bisimilar to the original Time Petri Net. As the method produce a single Timed Automaton, syntactical clocks reduction methods (DAWS and YOVINE for instance) may be applied to produce an automaton with fewer clocks. Then, our method allows to model-check T-TPN by the use of efficient Timed Automata tools.

Information

Type
Regular Papers
Copyright
2006 Cambridge University Press