A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking

  • Lasse Jacobsen
  • Morten Jacobsen
  • Mikael H. Møller
  • Jiří Srba
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6342)


Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment. The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that it preserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.


Integer Variable Abstract Syntax Atomic Proposition Variable Assignment Time Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)Google Scholar
  2. 2.
    Archer, M., HongPing, L., Lynch, N., Mitra, S., Umeno, S.: Specifying and proving properties of timed I/O automata in the TIOA toolkit. In: Proc. of MEMOCODE 2006, pp. 129–138 (2006)Google Scholar
  3. 3.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211–225. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between timed automata and bounded time Petri nets. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 82–97. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Bolognesi, T., Lucidi, F., Trigila, S.: From timed Petri nets to timed LOTOS. In: Proc. of PSTV 1990, pp. 395–408 (1990)Google Scholar
  7. 7.
    Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time Petri nets. Journal of Logic and Computation 19(6), 1509–1540 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Bouyer, P., Haddad, S., Reynier, P.A.: Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. Information and Computation 206(1), 73–107 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Byg, J., Joergensen, K.Y., Srba, J.: An efficient translation of timed-arc Petri nets to networks of timed automata. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 698–716. Springer, Heidelberg (2009)Google Scholar
  10. 10.
    Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. ENTCS 128(6), 145–160 (2005); Proc. of AVoCS 2004Google Scholar
  11. 11.
    Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed Automata Patterns. IEEE Transactions on Software Engingeering 34(6), 844–859 (2008)CrossRefGoogle Scholar
  12. 12.
    Gardey, G., Lime, D., Magnin, 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
  13. 13.
    Jacobsen, L., Jacobsen, M., Möller, M.H., Srba, J.: A framework for relating timed transition systems and preserving TCTL model checking. Technical Report FIMU-RS-2010-09, Faculty of Informatics, Masaryk Univ. (2010)Google Scholar
  14. 14.
    Janowska, A., Janowski, P., Wróblewski, D.: Translation of Intermediate Language to Timed Automata with Discrete Data. Fundamenta Informaticae 85(1-4), 235–248 (2008)MathSciNetzbMATHGoogle Scholar
  15. 15.
    Merlin, P.M.: A Study of the Recoverability of Computing Systems. PhD thesis, University of California, Irvine (1974)Google Scholar
  16. 16.
    Penczek, W., Pólrola, A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. SCI, vol. 20. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  17. 17.
    Sifakis, J., Yovine, S.: Compositional specification of timed systems. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 347–359. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  18. 18.
    Srba, J.: Timed-arc Petri nets vs. networks of timed automata. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 385–402. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Srba, J.: Comparing the expressiveness of timed automata and timed extensions of Petri nets. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 15–32. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Lasse Jacobsen
    • 1
  • Morten Jacobsen
    • 1
  • Mikael H. Møller
    • 1
  • Jiří Srba
    • 1
  1. 1.Department of Computer ScienceAalborg UniversityAalborg EastDenmark

Personalised recommendations