Time Petri Nets (TPN) and Timed Automata (TA) are widely-used formalisms for the modeling and analysis of timed systems. A recently-developed approach for the analysis of TPNs concerns their translation to TAs, at which point efficient analysis tools for TAs can then be applied. One feature of much of this previous work has been the use of timed reachability analysis on the TPN in order to construct the TA. In this paper we present a method for the translation from TPNs to TAs which bypasses the timed reachability analysis step. Instead, our method relies on the reachability graph of the underlying untimed Petri net. We show that our approach is competitive for the translation of a wide class of TPNs to TAs in comparison with previous approaches, both with regard to the time required to perform the translation, and with regard to the number of locations and clocks of the produced TA. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
D’Aprile, D., Donatelli, S., Sangnier, A., & Sproston, J. (2007). From time petri nets to timed automata: An untimed approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4424 LNCS, pp. 216–230). Springer Verlag. https://doi.org/10.1007/978-3-540-71209-1_18
Mendeley helps you to discover research relevant for your work.