[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A tableau calculus for first-order branching time logic

  • Conference paper
  • First Online:
Practical Reasoning (FAPR 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1085))

Included in the following conference series:

Abstract

Tableau-based proof systems have been designed for many logics extending classical first-order logic. This paper proposes a sound tableau calculus for temporal logics of the first-order CTL-family. Until now, a tableau calculus has only been presented for the propositional version of CTL. The calculus considered operates with prefixed formulas and may be regarded as an instance of a labelled deductive system. The prefixes allow an explicit partial description of states and paths of a potential Kripke counter model in the tableau. It is possible in particular to represent path segments of finite but arbitrary length which are needed to process reachability formulas. Furthermore, we show that by using prefixed formulas and explicit representation of paths it becomes possible to express and process fairness properties without having to resort to full CTL. The approach is suitable for use in interactive proof-systems.

Most of this work has been done while the first author was student at Universität Karlsruhe. At present his work at Universität Freiburg is supported by grant no. GRK 184/1-96 of the Deutsche Forschungsgemeinschaft.

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.

Similar content being viewed by others

References

  1. M. Ben-Ari, Z. Manna, A. Pnueli: The Temporal Logic of Branching Time. Proc. of the 8th ACM Symp. on Principles of Programming Languages, 1981.

    Google Scholar 

  2. E. M. Clarke, E. A. Emerson: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. Proc. of the IBM Workshop on Logics of Programs, Springer LNCS 131, 1981.

    Google Scholar 

  3. E. M. Clarke, E. A. Emerson, A. P. Sistla: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Tr. on Programming Languages and Systems, Vol. 8, No. 2, 1986.

    Google Scholar 

  4. E. A. Emerson, E. M. Clarke: Characterizing Properties of Parallel Programs as Fixpoints. Proc. of the 7th Int. Coll. on Automata, Languages and Programming. Springer LNCS 85, 1980.

    Google Scholar 

  5. E. A. Emerson, J. Y. Halpern: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. Proc. of the 14th ACM Symp. on Computing, 1982.

    Google Scholar 

  6. E. A. Emerson, J. Y. Halpern: “Sometimes” and “not never” revisited: On Branching Time versus Linear Time in Temporal Logic. Proc. of the 10th ACM Symp. on Principles of Programming Languages, 1983.

    Google Scholar 

  7. E. A. Emerson, C.-L. Lei: Modalities for Model Checking: Branching Time Strikes Back. Proc. of the 12th ACM Symp. on Principles of Programming Languages, 1985.

    Google Scholar 

  8. M. Fitting: First Order Logic and Automated Theorem Proving. Springer, New York, 1990.

    Google Scholar 

  9. D. M. Gabbay, I. Hodkinson, M. Reynolds: Temporal Logic. Mathematical Foundations and Computational Aspects. Vol. 1. Clarendon Press, Oxford Logic Guides No. 28, 1994.

    Google Scholar 

  10. L. Lamport: “Sometimes” is Sometimes “Not Never”. Proc. of the 7th ACM Symp. on Principles of Programming Languages, 1980.

    Google Scholar 

  11. D. Lehmann, A. Pnueli, J. Stavi: Impartiality, Justice, and Fairness: The Ethics of Concurrent Termination. Proc. of the 8th Int. Coll. on Automata, Languages and Programming. Springer LNCS 115, 1981.

    Google Scholar 

  12. W. May: Protokollverifikation in Temporallogik: Evolving Algebras und ein Tableaukalkül. Diplomarbeit, Universität Karlsruhe, 1995.

    Google Scholar 

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

    Google Scholar 

  14. S. V. Reeves: Semantic Tableaux as a Framework for Automated Theorem-Proving. Dept. of Comp. Sc. and Statistics, Queen Mary College, Univ. of London.

    Google Scholar 

  15. P. Wolper: The Tableau Method for Temporal Logic. Logique et Analyse, 110–111, vol. 28, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Freiburg, Germany

    Wolfgang May

  2. Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, Germany

    Peter H. Schmitt

Authors
  1. Wolfgang May
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter H. Schmitt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Dov M. Gabbay Hans Jürgen Ohlbach

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

May, W., Schmitt, P.H. (1996). A tableau calculus for first-order branching time logic. In: Gabbay, D.M., Ohlbach, H.J. (eds) Practical Reasoning. FAPR 1996. Lecture Notes in Computer Science, vol 1085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61313-7_89

Download citation

  • DOI: https://doi.org/10.1007/3-540-61313-7_89

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61313-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation