×

zbMATH — the first resource for mathematics

Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. (English) Zbl 1133.68053
Summary: Timed Petri nets and timed automata are two standard models for the analysis of real-time systems. We study in this paper their relationship, and prove in particular that they are incomparable with respect to language equivalence. In fact, we study the more general model of timed Petri nets with read-arcs (RA-TdPN), already introduced in [J. Srba, “Timed-arc Petri nets vs. networks of automata”, Lect. Notes Comput. Sci. 3536, 385–402 (2005; Zbl 1128.68069)], which unifies both models of timed Petri nets and of timed automata, and prove that the coverability problem remains decidable for this model. Then, we establish numerous expressiveness results and prove that Zeno behaviours discriminate between several sub-classes of RA-TdPNs. This has surprising consequences on timed automata, for instance, on the power of non-deterministic clock resets.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
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] Alur, R.; Dill, D., A theory of timed automata, Theoretical computer science, 126, 2, 183-235, (1994) · Zbl 0803.68071
[4] Berthomieu, B.; Diaz, M., Modeling and verification of time dependent systems using time Petri nets, IEEE transactions in software engineering, 17, 3, 259-273, (1991)
[5] Bouyer, P.; Dufourd, C.; Fleury, E.; Petit, A., Updatable timed automata, Theoretical computer science, 321, 2-3, 291-345, (2004) · Zbl 1070.68063
[6] 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
[7] Bouyer, P.; Haddad, S.; Reynier, P.-A., Timed unfoldings of networks of timed automata, (), 292-306 · Zbl 1161.68614
[8] C. Girault, R. Valk (Eds.), Petri Nets for Systems Engineering, Springer, Berlin, 2002.
[9] G. Higman, Ordering by divisibility in abstract algebras, in: Proceedings of the London Mathematical Society, vol. 2, 1952, pp. 326-336. · Zbl 0047.03402
[10] Laroussinie, F.; Markey, N.; Schnoebelen, Ph., Model checking timed automata with one or two clocks, (), 387-401 · Zbl 1099.68057
[11] S. Lasota, I. Walukiewicz, Alternating timed automata, in: Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’05), Lecture Notes in Computer Science, vol. 3441, Springer, Berlin, 2005, pp. 250-265. · Zbl 1119.68109
[12] P. Mahata, Model Checking Parameterized Timed Systems, PhD thesis, Department of Information Technology, Uppsala University, Uppsala, Sweden, 2005.
[13] McMillan, K., A technique of state space search based on unfolding, Formal methods in system design, 6, 1, 45-65, (1995) · Zbl 0829.68085
[14] Montanari, U.; Rossi, F., Contextual nets, Acta informatica, 32, 6, 545-596, (1995) · Zbl 0835.68084
[15] Ouaknine, J.; Worrell, J.B., On the language inclusion problem for timed automata: closing a decidability gap, (), 54-63
[16] Ouaknine, J.; Worrell, J.B., On the decidability of metric temporal logic, (), 188-197
[17] Srba, J., Timed-arc Petri nets vs networks of timed automata, (), 385-402 · Zbl 1128.68069
[18] Valero, V.; Frutos-Escrig, D.; Cuartero, F.R.F., On non-decidability of reachability for timed-arc Petri nets, (), 188-196
[19] Vogler, W., Efficiency of asynchronous systems, Read arcs, and the MUTEX-problem, Theoretical computer science, 275, 1-2, 589-631, (2002) · Zbl 1026.68099
[20] Vogler, W.; Semenov, A.L.; Yakovlev, A., Unfolding and finite prefix for nets with Read arcs, (), 501-516 · Zbl 0940.68096
[21] Winkowski, J., Reachability in contextual nets, Fundamenta informaticae, 51, 1-2, 235-250, (2002) · Zbl 1003.68106
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.