Skip to main content
SpringerLink
Log in

A (non-elementary) modular decision procedure for LTrL

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1998 (MFCS 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1450))

Abstract

Thiagarajan and Walukiewicz [18] have defined a temporal logic LTrL on Mazurkiewicz traces, patterned on the famous propositional temporal logic of linear time LTL defined by Pnueli. They have shown that this logic is equal in expressive power to the first order theory of finite and infinite traces.

The hopes to get an ”easy” decision procedure for LTrL, as it is the case for LTL, vanished very recently due to a result of Walukiewicz [19] who showed that the decision procedure for LTrL is non-elementary.

However, tools like Mona [8] or Mosel [7] show that it is possible to handle non-elementary logics on significant examples.

Therefore, it appears worthwhile to have a direct decision procedure for LTrL; in this paper we propose such a decision procedure, in a modular way. Since the logic LTrL is not pure future, our algorithm constructs by induction a finite family of Büchi automata for each LTrL-formula. As expected by the results of [19], the main difficulty comes from the ”Until” operator.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur, D. Peled, and W. Penczek. Model-checking of causality properties. In Proceedings of LICS'95, pages 90–100, 1995.

    Google Scholar 

  2. J.R. Büchi. Weak second-order arithmetic and finite automata. Z. Math Logik Grundlag. Math., 6:66–92, 1960.

    MATH  Google Scholar 

  3. C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. formal Methods in System Design, 1:275–288, 1992.

    Article  Google Scholar 

  4. V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.

    Google Scholar 

  5. W. Ebinger. Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. Dissertation, Institut für Informatik, Universität Stuttgart, 1994.

    Google Scholar 

  6. P. Gastin, R. Meyer, and A. Petit. A (non-elementary) modular decision procedure for LTrL. Technical report, LSV, ENS de Cachan, June 1998.

    Google Scholar 

  7. P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. Mosel: a flexible toolset for monadic second-order logic. In Proceedings of CAV'97, LNCS 1254, 1997.

    Google Scholar 

  8. N. Klarlund. Mona & Fido: The logic-automaton connection in practice. In Proceedings of CSL'97, LNCS, 1998.

    Google Scholar 

  9. A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.

    Google Scholar 

  10. R. Meyer and A. Petit. Expressive completeness of LTrL on finite traces: an algebraic proof. In Proceedings of STACS'98, number 1373 in LNCS, pages 533–543, 1998.

    MathSciNet  Google Scholar 

  11. D. Perrin and J. E. Pin. Infinite words. Technical report, LITP, Avril 1997.

    Google Scholar 

  12. A. Pnueli. The temporal logics of programs. In Proceedings of the 18th IEEE FOCS, 1977, pages 46–57, 1977.

    Google Scholar 

  13. R. Ramanujam. Locally linear time temporal logic. In Proceedings of LICS'96, pages 118–128, 1996.

    Google Scholar 

  14. S. Safra. On the complexity of Ω-automata. In Proceedings of the 29th annual IEEE Symp. on Foundations of Computer Science, pages 319–327, 1988.

    Google Scholar 

  15. A. Sistla and E. Clarke. The complexity of propositional linear time logic. J. ACM, 32:733–749, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  16. L. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, TR 133, M.I.T., Cambridge, 1974.

    Google Scholar 

  17. P. S. Thiagarajan. A trace based extension of linear time temporal logic. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS'94), pages 438–447, 1994.

    Google Scholar 

  18. P. S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for Mazurkiewicz traces. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97), 1997.

    Google Scholar 

  19. I. Walukiewicz. Difficult configurations — on the complexity of LTrL. In Proceedings of ICALP'98, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIAFA, Université Paris 7, 2, place Jussieu, P-75251, Paris Cedex 05

    Paul Gastin

  2. LSV, URA 2236 CNRS, ENS de Cachan, 61, av. du Prés Wilson, F-94235, Cachan Cedex

    Raphaël Meyer & Antoine Petit

Authors
  1. Paul Gastin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raphaël Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Antoine Petit
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Luboš Brim Jozef Gruska Jiří Zlatuška

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gastin, P., Meyer, R., Petit, A. (1998). A (non-elementary) modular decision procedure for LTrL. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055785

Download citation

  • DOI: https://doi.org/10.1007/BFb0055785

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64827-7

  • Online ISBN: 978-3-540-68532-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation