Advertisement

Comparison of the Expressiveness of Timed Automata and Time Petri Nets

  • Beatrice Bérard
  • Franck Cassez
  • Serge Haddad
  • Didier Lime
  • Olivier H. Roux
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)

Abstract

In this paper we consider the model of Time Petri Nets (TPN) where time is associated with transitions. We also consider Timed Automata (TA) as defined by Alur & Dill, and compare the expressiveness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove that there exists a TA \(\mathcal{A}\) s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to \(\mathcal{A}\). We then propose a structural translation from TA to (1-safe) TPNs preserving timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass \(\mathcal{T}_{syn}(\leq,\geq)\) of TA. For the theory of TPNs, the consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass \(\mathcal{T}_{syn}(\leq,\geq)\), bounded and 1-safe TPNs “à la Merlin” are equally expressive w.r.t. timed bisimilarity.

Keywords

Timed Language Timed Bisimilarity Time Petri Nets Timed Automata Expressiveness 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abdulla, P.A., Nylén, A.: Timed Petri nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–72. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    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, 7–51 (2002)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science B 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Alur, R., Fix, L., Henzinger, T.A.: Event-Clock Automata: A Determinizable Class of Timed Automata. Theoretical Computer Science 211, 253–273 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Aura, T., Lilius, J.: A causal semantics for time Petri nets. Theoretical Computer Science 243(1–2), 409–447 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – Construction of Abstract State Spaces for Petri Nets and Time Petri Nets. International Journal of Production Research 4(12) (July 2004)Google Scholar
  7. 7.
    Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the Expressiveness of Timed Automata and Time Petri Nets. Research Report IRCCyN R2005-2 (2005), available at http://www.lamsade.dauphine.fr/~haddad/publis.html
  8. 8.
    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)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Boyer, M., Diaz, M.: Non equivalence between time Petri nets and time stream Petri nets. In: Proceedings of 8th International Workshop on Petri Nets and Performance Modeling (PNPM 1999), Zaragoza, Spain, pp. 198–207 (1999)Google Scholar
  10. 10.
    Cassez, F., Roux, O.H.: Structural Translation of Time Petri Nets into Timed Automata. In: Huth, M. (ed.) Workshop on Automated Verification of Critical Systems (AVoCS 2004). Electronic Notes in Computer Science. Elsevier, Amsterdam (2004)Google Scholar
  11. 11.
    de Frutos Escrig, D., Valero Ruiz, V., Marroquín Alonso, O.: Decidability of properties of timed-arc Petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 187–206. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Diaz, M., Senac, P.: Time stream Petri nets: a model for timed multimedia information. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 219–238. Springer, Heidelberg (1994)Google Scholar
  13. 13.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)Google Scholar
  14. 14.
    Gardey, G., Lime, D., Magin, M., Roux, O.H.: Romeo: A Tool for Analyzing Time Petri Nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  15. 15.
    Haar, S., Simonot-Lion, F., Kaiser, L., Toussaint, J.: Equivalence of Timed State Machines and safe Time Petri Nets. In: Proceedings of WODES 2002, Zaragoza, Spain, pp. 119–126 (2002)Google Scholar
  16. 16.
    Khansa, W., Denat, J.P., Collart-Dutilleul, S.: P-Time Petri Nets for manufacturing systems. In: WODES 1996, Scotland, pp. 94–102 (1996)Google Scholar
  17. 17.
    Lime, D., Roux, O.H.: State class timed automaton of a time Petri net. In: PNPM 2003. IEEE Computer Society, Los Alamitos (2003)Google Scholar
  18. 18.
    Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, University of California, Irvine, CA (1974)Google Scholar
  19. 19.
    Pezzé, M., Young, M.: Time Petri Nets: A Primer Introduction. Tutorial presented at the Multi-Workshop on Formal Methods in Performance Evaluation and Applications, Zaragoza, Spain (September 1999)Google Scholar
  20. 20.
    Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA (1974)Google Scholar
  21. 21.
    Sifakis, J.: Performance Evaluation of Systems using Nets. In: Brauer, W. (ed.) Net Theory and Applications. LNCS, vol. 84, pp. 307–319. Springer, Heidelberg (1980)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Beatrice Bérard
    • 1
  • Franck Cassez
    • 2
  • Serge Haddad
    • 1
  • Didier Lime
    • 3
  • Olivier H. Roux
    • 2
  1. 1.LAMSADEParisFrance
  2. 2.IRCCyNNantesFrance
  3. 3.CISSAalborgDenmark

Personalised recommendations