×

zbMATH — the first resource for mathematics

When are timed automata weakly timed bisimilar to time Petri nets? (English) Zbl 1158.68029
Summary: We compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass \(\mathcal{TA}^{wtb}\) of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem for \(\mathcal{TA}^{wtb}\) are PSPACE-complete. Furthermore we show that for a TA in \(\mathcal{TA}^{wtb}\) with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential with respect to the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
Software:
Kronos; Romeo; TINA; Uppaal2k
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.A.; Mahata, P.; Mayr, R., Decidability of zenoness, syntactic boundedness and token-liveness for dense-timed Petri nets, (), 58-70 · Zbl 1117.68445
[2] Abdulla, P.A.; Nylén, A., Timed Petri nets and bqos, (), 53-70 · Zbl 0986.68092
[3] Aceto, L.; Laroussinie, F., Is your model checker on time? on the complexity of model checking for timed modal logics, Journal of logic and algebraic programming, 52-53, August, 7-51, (2002) · Zbl 1008.68030
[4] Alur, R.; Dill, D., A theory of timed automata, Theoretical computer science B, 126, 183-235, (1994) · Zbl 0803.68071
[5] Aura, T.; Lilius, J., A causal semantics for time Petri nets, Theoretical computer science, 243, 1-2, 409-447, (2000) · Zbl 0951.68095
[6] Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; Roux, O.H., Comparison of different semantics for time Petri nets, (), 293-307 · Zbl 1170.68537
[7] Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; Roux, O.H., Comparison of the expressiveness of timed automata and time Petri nets, (), 211-225 · Zbl 1175.68270
[8] Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; Roux, O.H., When are timed automata weakly timed bisimilar to time Petri nets?, (), 273-284 · Zbl 1158.68424
[9] Bérard, B.; Diekert, V.; Gastin, P.; Petit, A., Characterization of the expressive power of silent transitions in timed automata, Fundamenta informaticae, 36, 2-3, 145-182, (1998) · Zbl 0930.68077
[10] Berthomieu, B.; Diaz, M., Modeling and verification of time dependent systems using time Petri nets, IEEE transactions on software engineering, 17, 3, 259-273, (1991)
[11] Berthomieu, B.; Vernadat, F., Time Petri nets analysis with TINA, (), 123-124
[12] Bouyer, P., Forward analysis of updatable timed automata, Formal methods in system design, 24, 3, 281-320, (2004) · Zbl 1073.68041
[13] Bouyer, P.; Dufourd, C.; Fleury, E.; Petit, A., Updatable timed automata, Theoretical computer science, 321, 2-3, 291-345, (2004) · Zbl 1070.68063
[14] Bouyer, P.; Haddad, S.; Reynier, P.-A., Timed Petri nets and timed automata: on the discriminating power of Zeno sequences, (), 420-431 · Zbl 1133.68383
[15] P. Bouyer, S. Haddad, P.-A. Reynier, Undecidability results for timed automata with silent transitions, Research Report LSV-07-12. http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-12.pdf February 2007
[16] Bucci, G.; Fedeli, A.; Sassoli, L.; Vicario, E., Timed state space analysis of real-time preemptive systems, IEEE transactions on software engineering, 30, 2, 97-111, (2004)
[17] Cassez, F.; Roux, O.H., Structural translation of time Petri nets into timed automata — model-checking time Petri nets via timed automata, The journal of systems and software, 79, 10, 1456-1468, (2006)
[18] Dill, D.L., Timing assumptions and verification of finite-state concurrent systems, (), 197-212
[19] Gardey, G.; Lime, D.; Magnin, M.; Roux, O.H., Roméo: A tool for analyzing time Petri nets, (), 418-423 · Zbl 1081.68618
[20] S. Haar, F. Simonot-Lion, L. Kaiser, J. Toussaint, Equivalence of timed state machines and safe time petri nets, in: Proceedings of 6th International Workshop on Discrete Event Systems, WODES 2002, Zaragoza, Spain, 2002, pp. 119-126
[21] Henzinger, T.A.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Information and computation, 111, 2, 193-244, (1994) · Zbl 0806.68080
[22] Lime, D.; Roux, O.H., State class timed automaton of a time Petri net, (), 124-133
[23] Nicollin, X.; Sifakis, J., An overview and synthesis on timed process algebras, (), 376-398
[24] P.M. Merlin, A study of the recoverability of computing systems, Ph.D. Thesis, University of California, Irvine, CA, 1974
[25] Pettersson, P.; Larsen, K.G., \scuppaal 2k, Bulletin of the European association for theoretical computer science, 70, February, 40-44, (2000)
[26] Popova-Zeugmann, L.; Heiner, M.; Koch, I., Time Petri nets for modelling and analysis of biochemical networks, Fundamenta informaticae (FI), 67, 149-162, (2005) · Zbl 1096.68110
[27] C. Ramchandani, Analysis of asynchronous concurrent systems by timed Petri nets, Ph.D. Thesis, Massachusetts Institute of Technology, Cambridge, MA, 1974
[28] Yovine, S., Kronos: A verification tool for real-time systems, Journal of software tools for technology transfer, 1, 1-2, 123-133, (1997) · Zbl 1060.68606
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.