Skip to main content
SpringerLink
Log in

Difficult configurations — on the complexity of LTrL

Extended abstract

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1998)

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

Included in the following conference series:

Abstract

The complexity of LTrL, a global linear time temporal logic over traces is investigated. The logic is global because the truth of a formula is evaluated in a global state, also called configuration. The logic is shown to be non-elementary with the main reason for this complexity being the nesting of until operators in formulas. The fragment of the logic without the until operator is shown to be EXPSPACE-complete.

Supported by Polish KBN Kraut No. 8 T11C 002 11

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, K. McMillan, and D. Peled. Deciding global parial-order properties. submitted, 1997.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  4. W. Ebinger and A. Muscholl. Logical definability on infinite traces. In ICALP '93, volume 700, pages 335–346, 1993

    MathSciNet  Google Scholar 

  5. P. Godefroid. Partial-order methods for the verification of concurrent systems, volume 1032 of LNCS. Springer-Verlag, 1996.

    Google Scholar 

  6. G. K. Lodaya, R. Parikh, R. Ramanujam, and P. Thiagarajan. A logical study of distributed transition systems. Information and Computation, 119:91–118, 1985.

    Article  MathSciNet  Google Scholar 

  7. D. Peled. Partial order reduction: model checking using representatives. In MFCS'96, volume 1113 of LNCS, pages 93–112, 1996.

    MathSciNet  Google Scholar 

  8. D. Peled and A. Pnueli. Proving partial order properties. Theoretical Computer Science, 126:143–182, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  9. W. Penczek. On udecidability of prepositional temporal logics on trace systems. Information Processing Letters, 43:147–153, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  10. R. Ramanujam. Locally linear time temporal logic. In LICS '96, pages 118–128, 1990.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  12. P. S. Thiagarajan. A trace based extension of linear time temporal logic. In LICS, pages 438–447, 1994.

    Google Scholar 

  13. P. S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for mazurkiewicz traces. In LICS'97, pages 183–194. IEEE, 1997.

    Google Scholar 

  14. A. Valmari. A stubborn attack on state explosion. Formal Methods in System, Design, 1:297–322, 1992.

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, Warsaw University, Banacha 2, 02-097, Warsaw, Poland

    Igor Walukiewicz

Authors
  1. Igor Walukiewicz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Kim G. Larsen Sven Skyum Glynn Winskel

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Walukiewicz, I. (1998). Difficult configurations — on the complexity of LTrL . In: Larsen, K.G., Skyum, S., Winskel, G. (eds) Automata, Languages and Programming. ICALP 1998. Lecture Notes in Computer Science, vol 1443. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055048

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64781-2

  • Online ISBN: 978-3-540-68681-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation