State Space Computation and Analysis of Time Petri Nets
| dc.creator | Gardey, Guillaume | |
| dc.creator | Roux, Olivier H. | |
| dc.creator | Roux, Olivier F. | |
| dc.date | 2005-05-10 | |
| dc.date.accessioned | 2026-07-07T03:22:58Z | |
| dc.date.available | 2026-07-07T03:22:58Z | |
| dc.description | 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 TTPN by the use of efficient Timed Automata tools. To appear in Theory and Practice of Logic Programming (TPLP). | |
| dc.description | 21 pages | |
| dc.identifier | https://arxiv.org/abs/cs/0505023 | |
| dc.identifier | http://arxiv.org/abs/cs/0505023 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/32762 | |
| dc.subject | Logic in Computer Science | |
| dc.title | State Space Computation and Analysis of Time Petri Nets | |
| dc.type | text |