[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences

  • Conference paper
Automata, Languages and Programming (ICALP 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4052))

Included in the following conference series:

  • 6126 Accesses

Abstract

Timed Petri nets and timed automata are two standard models for the analysis of real-time systems. In this paper, we prove that they are incomparable for the timed language equivalence. Thus we propose an extension of timed Petri nets with read-arcs (RA-TdPN), whose coverability problem is decidable. We also show that this model unifies timed Petri nets and timed automata. 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, e.g. on the power of non-deterministic clock resets.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abdulla, P.A., Mahata, P., Mayr, R.: Decidability of Zenoness, syntactic boundedness and token-liveness for dense-timed petri nets. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 58–70. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Abdulla, P.A., Nylén, A.: Timed Petri nets and bqos. In Proc. 22nd Int. Conf. Application and Theory of Petri Nets (ICATPN’01). In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–70. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  5. Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theoretical Computer Science 321(2–3), 291–345 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  6. Bouyer, P., Haddad, S., Reynier, P.-A.: Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. In: Research Report LSV-06-06, ENS de Cachan, France (2006)

    Google Scholar 

  7. Bouyer, P., Haddad, S., Reynier, P.-A.: Timed unfoldings of networks of timed automata. In: Research Report LSV-06-09, ENS de Cachan, France (2006)

    Google Scholar 

  8. Girault, C., Valk, R. (eds.): Petri Nets for Systems Engineering. Springer, Heidelberg (2002)

    Google Scholar 

  9. Mahata, P.: Model Checking Parameterized Timed Systems. PhD thesis, Dept. Information Technology, Uppsala University, Sweden (2005)

    Google Scholar 

  10. Montanari, U., Rossi, F.: Contextual nets. Acta Informatica 32(6), 545–596 (1995)

    MATH  MathSciNet  Google Scholar 

  11. Srba, J.: Timed-arc Petri nets vs. networks of timed automata. In Proc. 26th International Conference Application and Theory of Petri Nets (ICATPN’05). In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 385–402. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Valero Ruiz, V., Cuartero Gomez, F., de Frutos-Escrig, D.: On non-decidability of reachability for timed-arc Petri nets. In: Proc. 8th Int. Work. Petri Nets and Performance Models (PNPM 2003), pp. 188–196. IEEE Computer Society Press, Los Alamitos (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bouyer, P., Haddad, S., Reynier, PA. (2006). Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds) Automata, Languages and Programming. ICALP 2006. Lecture Notes in Computer Science, vol 4052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11787006_36

Download citation

  • DOI: https://doi.org/10.1007/11787006_36

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-35907-4

  • Online ISBN: 978-3-540-35908-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics