Skip to main content

Expressive completeness of Temporal Logic of action

  • 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

The paper compares the expressive power of monadic second order logic of order, a fundamental formalism in mathematical logic and theory of computation, with that of a fragment of Temporal Logic of Actions introduced by Lamport for specifying the behavior of concurrent systems.

Supported by a research grant of Tel Aviv University.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. R. Büchi. On a decision method in restricted second order arithmetic In Proc. International Congress on Logic, Methodology and Philosophy of Science, E. Nagel at al. eds, Stanford University Press, pp 1–11, 1960.

    Google Scholar 

  2. L. Lamport. What good is temporal logic. In R. E. A. Manson editor Information Processing 83, Proceedings of IFIP 9th World Congress, Paris pp. 657–668. IFIP, North Holland.

    Google Scholar 

  3. L. Lamport. The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3), pp. 872–923, 1994.

    Article  Google Scholar 

  4. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems, Springer Verlag, 1992.

    Google Scholar 

  5. M. O. Rabin. Decidable theories. In J. Barwise editor Handbook of Mathematical Logic, North-Holland, 1977.

    Google Scholar 

  6. A. Rabinovich. On Translations of Temporal Logic of Actions into Monadic Second Order Logic. Theoretical Computer Science 193 (1998), 197–214.

    Article  MATH  MathSciNet  Google Scholar 

  7. A. Rabinovich and B. A. Trakhtenbrot. From Finite Automata to Hybrid Systems. Fundamentals of Computation Theory 1997, LNCS vol. 1279, pages 411–422, 1997.

    MathSciNet  Google Scholar 

  8. W. Thomas. Automata on Infinite Objects. In J. van Leeuwen editor Handbook of Theoretical Computer Science, The MIT Press, 1990.

    Google Scholar 

  9. B. A. Trakhtenbrot and Y. M. Barzdin. Finite Automata, North Holland Amsterdam, 1973.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

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

Rabinovich, A. (1998). Expressive completeness of Temporal Logic of action. 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/BFb0055772

Download citation

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

  • 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