Advertisement

Pure Future Local Temporal Logics Are Expressively Complete for Mazurkiewicz Traces

  • Volker Diekert
  • Paul Gastin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2976)

Abstract

The paper settles a long standing problem for Mazurkiewicz traces: the pure future local temporal logic defined with the basic modalities exists-next and until is expressively complete. The analogous result with a global interpretation was solved some years ago by Thiagarajan and Walukiewicz (1997) and in its final form without any reference to past tense constants by Diekert and Gastin (2000). Each, the (previously known) global or the (new) local result generalizes Kamp’s Theorem for words, because for sequences local and global viewpoints coincide. But traces are labelled partial orders and then the difference between an interpretation globally over cuts (configurations) or locally at points (events) is significant. For global temporal logics the satisfiability problem is non-elementary (Walukiewicz 1998), whereas for local temporal logics both the satisfiability problem and the model checking problem are solvable in Pspace (Gastin and Kuske 2003) as in the case of words. This makes local temporal logics much more attractive.

Keywords

Temporal logics Mazurkiewicz traces concurrency 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Adsul, B., Sohoni, M.: Complete and tractable local linear time temporal logics over traces. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 926–937. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Peled, D., Penczek, W.: Model-checking of causality properties. In: Proc. of LICS 1995, pp. 90–100 (1995)Google Scholar
  3. 3.
    Diekert, V.: A pure future local temporal logic beyond cograph-monoids. In: Ito, M. (ed.) Proc. of the RIMS Symposium on Algebraic Systems, Formal Languages and Conventional and Unconventional Computation Theory, Kyoto, Japan (2002)Google Scholar
  4. 4.
    Diekert, V., Gastin, P.: LTL is expressively complete for Mazurkiewicz traces. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 211–222. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Diekert, V., Gastin, P.: Local temporal logic is expressively complete for cograph dependence alphabets. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 55–69. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Diekert, V., Gastin, P.: LTL is expressively complete for Mazurkiewicz traces. Journal of Computer and System Sciences 64, 396–418 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific, Singapore (1995)Google Scholar
  8. 8.
    Ebinger, W.: Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. Dissertation, Institut für Informatik, Universität Stuttgart (1994)Google Scholar
  9. 9.
    Ebinger, W., Muscholl, A.: Logical definability on infinite traces. Theoretical Computer Science 154, 67–84 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Gastin, P., Kuske, D.: Satisfiability and model checking for MSO-definable temporal logics are in PSPACE. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 222–236. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Gastin, P., Mukund, M.: An elementary expressively complete temporal logic for Mazurkiewicz traces. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 938–949. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Gastin, P., Mukund, M., Narayan Kumar, K.: Local LTL with past constants is expressively complete for Mazurkiewicz traces. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 429–438. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, California (1968)Google Scholar
  14. 14.
    Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus (1977)Google Scholar
  15. 15.
    Mukund, M., Thiagarajan, P.S.: Linear time temporal logics over Mazurkiewicz traces. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 62–92. Springer, Heidelberg (1996)Google Scholar
  16. 16.
    Niebert, P.: A ν-calculus with local views for sequential agents. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 563–573. Springer, Heidelberg (1995)Google Scholar
  17. 17.
    Penczek, W.: Temporal logics for trace systems: On automated verification. International Journal of Foundations of Computer Science 4, 31–67 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Ramanujam, R.: Locally linear time temporal logic. In: Proc. of LICS 1996, pp. 118–128 (1996)Google Scholar
  19. 19.
    Thiagarajan, P.S.: A trace based extension of linear time temporal logic. In: Proc. of LICS 1994, pp. 438–447. IEEE Computer Society Press, Los Alamitos (1994)Google Scholar
  20. 20.
    Thiagarajan, P.S., Walukiewicz, I.: An expressively complete linear time temporal logic for Mazurkiewicz traces. In: Proc. of LICS 1997, pp. 183–194 (1997)Google Scholar
  21. 21.
    Walukiewicz, A.: Difficult configurations – on the complexity of LTrL. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 140–151. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Volker Diekert
    • 1
  • Paul Gastin
    • 2
  1. 1.FMI, Universität StuttgartStuttgart
  2. 2.LIAFA, Université Paris 7Paris Cedex 05

Personalised recommendations