Abstract
Several formalisms to model distributed real-time systems coexist in the literature. This naturally induces a need to compare their expressiveness and to translate models from one formalism to another when possible. The first formal comparisons of the expressiveness of these models focused on the preservation of the sequential behavior of the models, using notions like timed language equivalence or timed bisimilarity. They do not consider preservation of concurrency. In this paper we define timed traces as a partial order representation of executions of our models for real-time distributed systems. Timed traces provide an alternative to timed words, and take the distribution of actions into account. We propose a translation between two popular formalisms that describe timed concurrent systems: 1-bounded time Petri nets (TPN) and networks of timed automata (NTA). Our translation preserves the distribution of actions, that is we require that if the TPN represents the product of several components (called processes), then each process should have its counterpart as one timed automaton in the resulting NTA.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Akshay S, Bollig B, Gastin P (2007) Automata and logics for timed message sequence charts. In: Foundations of software technology and theoretical computer science (FSTTCS). LNCS, vol 4855. Springer, New Delhi, pp 290–302
Akshay S, Bollig B, Gastin P, Mukund M, Narayan Kumar K (2008) Distributed timed automata with independently evolving clocks. In: International conference on concurrency theory (CONCUR). LNCS, vol 5201. Springer, Toronto, pp 82–97
Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183–235
Balaguer S, Chatain Th, Haar S (2010) A concurrency-preserving translation from time Petri nets to networks of timed automata. In: International symposium on temporal representation and reasoning (TIME). IEEE Computer Society Press, Paris, pp 77–84
Bérard B, Cassez F, Haddad S, Lime D, Roux OH (2008) When are timed automata weakly timed bisimilar to time Petri nets? Theor Comput Sci 403(2–3):202–220
Berthomieu B, Diaz M (1991) Modeling and verification of time dependent systems using time Petri nets. IEEE Trans Softw Eng 17(3):259–273
Berthomieu B, Ribet PO, Vernadat F (2004) The tool TINA—construction of abstract state spaces for Petri nets and time Petri nets. Int J Prod Res 42(14):2741–2756
Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: a model-checking tool for real-time systems. In: International conference on computer aided verification (CAV). LNCS, vol 1427, pp 546–550
Byg J, Joergensen K, Srba J (2009) An efficient translation of timed-arc Petri nets to networks of timed automata. In: International conference on formal engineering methods. LNCS, vol 5885. Springer, Berlin, pp 698–716
Cassez F, Roux OH (2006) Structural translation from time Petri nets to timed automata. J Syst Softw
Cerans K, Godskesen JC, Larsen KG (1993) Timed modal specification—theory and tools. In: International conference on computer aided verification (CAV). LNCS, vol 697. Springer, Berlin, pp 253–267
Colom JM, Silva M (1991) Convex geometry and semiflows in P/T nets. A comparative study of algorithms for computation of minimal p-semiflows. In: Proceedings of the 10th international conference on applications and theory of Petri nets. Springer, London, pp 79–112
Desel J, Esparza J (1995) Free choice Petri nets. Cambridge University Press, New York
Diekert V, Rozenberg G (1995) The book of traces. World Scientific Publishing Co, Inc, River Edge
Gardey G, Lime D, Magnin M, Roux OH (2005) Romeo: A tool for analyzing time Petri nets. In: International conference on computer aided verification (CAV). LNCS, vol 3576. Springer, Berlin, pp 418–423
Gardey G, Roux OH, Roux OF (2006) State space computation and analysis of time Petri nets. Theory Pract Log Program 6(3):301–320
Hack M (1972) Analysis of production schemata by Petri nets. Master’s thesis, Massachusetts Institute of Technology, Cambridge, USA
Henzinger TA, Kopke PW, Wong-Toi H (1995) The expressive power of clocks. In: International colloquium on automata, languages and programming (ICALP), pp 417–428
Jensen K, Kristensen LM, Wells L (2007) Coloured Petri nets and cpn tools for modelling and validation of concurrent systems. Int J Softw Tools Technol Transf 9(3–4):213–254
Lanotte R, Maggiolo-Schettini A, Peron A (2000) Timed cooperating automata. Fundam Inform 43:153–173
Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Softw Tools Technol Transf 1(1–2):134–152
Lautenbach K (1975) Liveness in Petri nets. Tech rep, Gesellschaft für Mathematik und Datenverarbeitung, Bonn, Germany
Lime D, Roux OH (2006) Model checking of time Petri nets using the state class timed automaton. J Discrete Event Dyn Syst 16(2):179–205
Lugiez D, Niebert P, Zennou S (2005) A partial order semantics approach to the clock explosion problem of timed automata. Theor Comput Sci 345(1):27–59
Merlin PM (1974) A study of the recoverability of computing systems. PhD thesis, University of California, Irvine
Niebert P, Qu H (2006) Adding invariants to event zone automata. In: International conference on formal modelling and analysis of timed systems (FORMATS). LNCS, vol 4202. Springer, Berlin, pp 290–305
Sifakis J, Yovine S (1996) Compositional specification of timed systems (extended abstract). In: Symposium on theoretical aspects of computer science (STACS). Springer, London, pp 347–359
Acknowledgements
This work is partially supported by the FARMAN project EMoTiCon funded by ENS Cachan and the French ANR projects DOTS and ImpRo.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Balaguer, S., Chatain, T. & Haar, S. A concurrency-preserving translation from time Petri nets to networks of timed automata. Form Methods Syst Des 40, 330–355 (2012). https://doi.org/10.1007/s10703-012-0146-4
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-012-0146-4