Interval Temporal Logic Semantics of Box Algebra

  • Hanna Klaudel
  • Maciej Koutny
  • Zhenhua Duan
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8370)


By focusing on two specific formalisms, viz. Box Algebra and Interval Temporal Logic, we extend the recently introduced translation of Petri nets into behaviourally equivalent logic formulas. We remove restrictions concerning the way in which the control flow of a concurrent system is modelled, and allow for a fully general synchronisation operator. Crucially, we strengthen the notion of equivalence between a Petri net and the corresponding logic formula, by proving such an equivalence at the level of transition based executions of Petri nets, rather than just by considering their labels.


Interval Temporal Logic Box Algebra Petri net composition semantics general synchronisation step sequence equivalence 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. In: White, J., Lipton, R.J., Goldberg, P.C. (eds.), pp. 164–176. ACM Press (1981)Google Scholar
  2. 2.
    Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. Springer (2001)Google Scholar
  3. 3.
    Cau, A., Zedan, H.: Refining interval temporal logic specifications. In: Rus, T., Bertrán, M. (eds.) AMAST-ARTS 1997, ARTS 1997, and AMAST-WS 1997. LNCS, vol. 1231, pp. 79–94. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  4. 4.
    Desel, J., Juhás, G.: What is a petri net? In: Ehrig, H., Juhás, G., Padberg, J., Rozenberg, G. (eds.) Unifying Petri Nets. LNCS, vol. 2128, pp. 1–25. Springer, Heidelberg (2001)Google Scholar
  5. 5.
    Duan, Z., Klaudel, H., Koutny, M.: ITL semantics of composite Petri nets. J. Log. Algebr. Program 82(2), 95–110 (2013)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Esparza, J.: Model checking using net unfoldings. Sci. Comput. Program. 23(2-3), 151–195 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Janicke, H., Cau, A., Siewe, F., Zedan, H.: Dynamic access control policies: Specification and verification. Comput. J. 56(4), 440–463 (2013)CrossRefGoogle Scholar
  9. 9.
    Khomenko, V., Koutny, M.: Towards an efficient algorithm for unfolding petri nets. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 366–380. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Moszkowski, B.C.: Executing Temporal Logic Programs. Cambridge University Press (1986)Google Scholar
  11. 11.
    Moszkowski, B.C.: A complete axiom system for propositional interval temporal logic with infinite time. Logical Methods in Computer Science 8(3) (2012)Google Scholar
  12. 12.
    Moszkowski, B.C., Manna, Z.: Reasoning in interval temporal logic. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 371–382. Springer, Heidelberg (1984)CrossRefGoogle Scholar
  13. 13.
    Parigot, M., Pelz, E.: A logical approach of Petri net languages. Theor. Comput. Sci. 39, 155–169 (1985)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Silva, M., Teruel, E., Colom, J.M.: Linear algebraic and linear programming techniques for the analysis of place/transition net systems. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 309–373. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  15. 15.
    Valmari, A., Hansen, H.: Can stubborn sets be optimal? Fundam. Inform. 113(3-4), 377–397 (2011)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Hanna Klaudel
    • 1
  • Maciej Koutny
    • 2
  • Zhenhua Duan
    • 3
  1. 1.IBISCUniversité d’Évry-Val-d’EssonneÉvry CedexFrance
  2. 2.School of Computing ScienceNewcastle University Claremont TowerUK
  3. 3.Institute of Computing Theory and TechnologyXidian UniversityXi’anP.R. China

Personalised recommendations