Skip to main content
SpringerLink
Log in

The complexity of propositional linear temporal logics in simple cases

(Extended abstract)

  • Logic I
  • Conference paper
  • First Online:
STACS 98 (STACS 1998)

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

Included in the following conference series:

Abstract

It is well-known that model-checking and satisfiability for PLTL are PSPACE-complete. By contrast, very little is known about whether there exist some interesting fragments of PLTL with a lower worst-case complexity. Such results would help understand why PLTL model-checkers are successfully used in practice.

In this paper we investigate this issue and consider model-checking and satisfiability for all fragments of PLTL one obtains when restrictions are put on (1) the temporal connectives allowed, (2) the number of atomic propositions, and (3) the temporal height.

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. C.-C. Chen and I. P. Lin. The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic. Information Processing Letters, 45(3):131–136, March 1993.

    Article  MATH  MathSciNet  Google Scholar 

  2. C. Dixon, M. Fisher, and M. Reynolds. Execution and proof in a Horn-clause temporal logic. In Proc. 2nd Int. Conf. on Temporal Logic (ICTL'97), Manchester, UK, July 1997, 1997. to appear.

    Google Scholar 

  3. S. Demri and Ph. Schnoebelen. The complexity of propositional linear temporal logics in simple cases. Research Report LSV-97-11, Lab. Specification and Verification, ENS de Cachan, Cachan, France, December 1997. Available at http://www.lsv.ens-cachan.fr/tphs. 1

    Google Scholar 

  4. E. A. Emerson, M. Evangelist, and J. Srinivasan. On the limits of efficient temporal decidability. In Proc. 5th IEEE Symp. Logic in Computer Science (LICS'90), Philadelphia, PA, USA, June 1990, pages 464–475, 1990.

    Google Scholar 

  5. E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275–306, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  6. E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, chapter 16, pages 995–1072. Elsevier Science Publishers, 1990.

    Google Scholar 

  7. J. Y. Halpern. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence, 75(2):361–372, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  8. D. Harel. Recurring dominos: Making the highly undecidable highly understandable. Annals of Discrete Mathematics, 24:51–72, 1985.

    MATH  MathSciNet  Google Scholar 

  9. J. Y. Halpern and J. H. Reif. The propositional dynamic logic of deterministic, well-structured programs. Theor. Comp. Sci., 27(1–2):127–165, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  10. D. S. Johnson. A catalog of complexity classes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. A, chapter 2, pages 67–161. Elsevier Science Publishers, 1990.

    Google Scholar 

  11. L. Lamport. What good is temporal logic ? In R. E. A. Mason, editor, Information Processing'83. Proc. IFIP 9th World Computer Congress, Sep. 1983, Paris, France, pages 657–668. North-Holland, 1983.

    Google Scholar 

  12. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.

    Google Scholar 

  13. A. Nakamura and H. Ono. On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica, 39(4):325–333, 1980.

    Article  MATH  MathSciNet  Google Scholar 

  14. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733–749, July 1985.

    Article  MATH  MathSciNet  Google Scholar 

  15. E. Spaan. Complexity Logics. PhD thesis, ILLC, Amsterdam University, NL, March 1993.

    Google Scholar 

  16. P. Wolper, M. Y. Vardi, and A. P. Sistla. Reasoning about infinite computation paths (extended abstract). In Proc. 24th IEEE Symp. Found. of Computer Science (FOCS'83), Tucson, USA, Nov. 1983, pages 185–194, 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Leibniz-IMAG, Univ. Grenoble & CNRS UMR 5522, 46, av. Félix Viallet, 38031, Grenoble Cedex, France

    S. Demri

  2. Lab. Specification and Verification, ENS de Cachait & CNRS URA 2236, 61, av. Pdt. Wilson, 94235, Cachan Cedex, France

    Ph. Schnoebelen

Authors
  1. S. Demri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ph. Schnoebelen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michel Morvan Christoph Meinel Daniel Krob

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag

About this paper

Cite this paper

Demri, S., Schnoebelen, P. (1998). The complexity of propositional linear temporal logics in simple cases. In: Morvan, M., Meinel, C., Krob, D. (eds) STACS 98. STACS 1998. Lecture Notes in Computer Science, vol 1373. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028549

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64230-5

  • Online ISBN: 978-3-540-69705-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation