Skip to main content
SpringerLink
Log in

Advanced Tense Logic

  • Chapter
Handbook of Philosophical Logic

Part of the book series: Handbook of Philosophical Logic ((HALO,volume 7))

Abstract

In this chapter we consider the tense (or temporal) logic with until and since connectives over general linear time. We will call this logic US/LT. This logic is an extension of Prior’s original temporal logic of F and P over linear time [Prior, 1957], via the introduction of the more expressive connectives of Kamp’s U for “until” and S for “since” [Kamp, 1968b]. U closely mimics the natural language construct “until” with U(A, B) holding when A is constantly true from now up until a future time at which B holds. S is similar with respect to the past. We will see that U and S do indeed extend the expressivemess of the temporal language.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Bibliography

  1. A. Amir. Separation in nonlinear time models. Information and Control, 66:177–203, 1985.

    Article  Google Scholar 

  2. B. Bannieqbal and H. Barringer. A study of an extended temporal language and a temporal fixed point calculus. Technical Report UMCS-86–10–2, Department of Computer Science, University of Manchester, 1986.

    Google Scholar 

  3. N. Belnap and M. Green. Indeterminism and the red thin line. In Philosophical Perspectives, 8, Logic and LanguaQe, pages 365–388. 1994.

    Google Scholar 

  4. J. Brzozowski and E. Leiss. Finite automata, and sequential networks. TCS, 10, 1980.

    Google Scholar 

  5. J.R. Büchi. On a decision method in restricted second order arithmetic. In Logic, Methodology, and Philosophy of Science: Proc. 1960 Intern. Congress, pages 1–11. Stanford University Press, 1962.

    Google Scholar 

  6. R. Bull and K. Segerberg. Basic modal logic. In D.M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, second edition, volume 2, page ? Kluwer, in this handbook.

    Google Scholar 

  7. J. Burgess. Basic tense logic. In D.M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, second edition, volume 7, pp. 1–42, Kluwer, 2001.

    Google Scholar 

  8. J. P. Burgess and Y. Gurevich. The decision problem for linear temporal logic. Notre Dame J. Formal Logic, 26(2):115–128, 1985.

    Article  Google Scholar 

  9. J. P. Burgess. Axioms for tense logic I: ‘since’ and ‘until’. Notre Dame J. Formal Logic, 23(2):367–374, 1982.

    Article  Google Scholar 

  10. Y. Choueka. Theories of automata on w-tapes: A simplified approach. JCSS, 8:117–141, 1974.

    Google Scholar 

  11. J. Darlington and L. While. Controlling the behaviour of functional programs. In Third Conference on Functional Programming Languages and Computer Architecture, 1987.

    Google Scholar 

  12. K. Doets. Monadic ∏i-theories of ∏i-properties. Notre Dame J. Formal Logic, 30:224–240, 1989.

    Article  Google Scholar 

  13. A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fund. Math., 49:128–141, 1961.

    Google Scholar 

  14. E. Emerson and C. Lei. Modalities for model checking: branching time strikes back. In Proc. 12th ACM Symp. Princ. Frog. Lang., pages 84–96, 1985.

    Google Scholar 

  15. E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B. Elsevier, Amsterdam, 1990.

    Google Scholar 

  16. K. Fine and G. Schurz. Transfer theorems for stratified multimodal logics. 1991.

    Google Scholar 

  17. M. Finger and D. M. Gabbay. Adding a Temporal Dimension to a Logic System. Journal of Logic Language and Information, 1:203–233, 1992.

    Article  Google Scholar 

  18. M. Finger and D. Gabbay. Combining Temporal Logic Systems. Notre Dame Journal of Formal Logic, 37(2):204–232, 1996. Special Issue on Combining Logics.

    Article  Google Scholar 

  19. M. Finger. Handling Database Updates in Two-dimensional Temporal Logic. J. of Applied Non-Classical Logic, 2(2):201–224, 1992.

    Article  Google Scholar 

  20. M. Finger. Changing the Past: Database Applications of Twodimensional Temporal Logics. PhD thesis, Imperial College, Department of Computing, February 1994.

    Google Scholar 

  21. M. Fisher. A normal form for tempral logic and its application in theoremproving and execution. Journal of Logic and Computation, 7(4):5, 1997.

    Article  Google Scholar 

  22. D. M. Gabbay and I. M. Hodkinson. An axiomatisation of the temporal logic with until and since over the real numbers. Journal of Logic and Computation, 1(2):229–260, 1990.

    Article  Google Scholar 

  23. D. M. Gabbay and N. Olivetti. Goal Directed Algorithmic Proof. APL Series, Kluwer, Dordrecht, 2000.

    Google Scholar 

  24. D. Gabbay and V. Shehtman. Products of modal logics, part 1. Logic Journal of the IGPL, 6(1):73–146, 1998.

    Article  Google Scholar 

  25. D. M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In 7th ACM Symposium on Principles of Programming Languages, Las Vegas, pages 163–173, 1980.

    Google Scholar 

  26. D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1. Oxford University Press, 1994.

    Google Scholar 

  27. D. Gabbay, M. Reynolds, and M. Finger. Temporal Logic: Mathematical Foundations and Computational Aspects, Vol. 2. Oxford University Press, 2000.

    Google Scholar 

  28. D. M. Gabbay. An irreflexivity lemma with applications to axiomatizations of conditions on tense frames. In U. Monnich, editor, Aspects of Philosophical Logic, pages 67–89. Reidel, Dordrecht, 1981.

    Chapter  Google Scholar 

  29. D. Gabbay. N-Prolog, part 2. Journal of Logic Programming, 5:251–283, 1985.

    Article  Google Scholar 

  30. D. M. Gabbay. Declarative past and imperative future: Executable temporal logic for interactive systems. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proceedings of Colloquium on Temporal Logic in Specification, Altrincham, 1987, pages 67–89. Springer-Verlag, 1989. Springer Lecture Notes in Computer Science

    Google Scholar 

  31. D. M. Gabbay. Labelled Deductive Systems. Oxford University Press, 1996.

    Google Scholar 

  32. D. M. Gabbay. Fibring Logics. Oxford University Press, 1998.

    Google Scholar 

  33. D. M. Gabbay, A. Kurucz, F. Wolter and M. Zakharyaschev. Many Dimensional Logics, Elsevier, 2002. To appear.

    Google Scholar 

  34. Y. Gurevich. Elementary properties of ordered abelian groups. Algebra and Logic, 3:5–39, 1964. (Russian; an English version is in Trans. Amer. Math. Soc. 46 (1965), 165–192).

    Google Scholar 

  35. Y. Gurevich. Monadic second-order theories. In J. Barwise and S. Feferman, editors, Model- Theoretic Logics, pages 479–507. Springer-Verlag, New York, 1985.

    Google Scholar 

  36. W. Hodges. Logical features of horn clauses. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, The Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 1, pages 449–504. Oxford University Press, 1985.

    Google Scholar 

  37. I. Hodkinson. Decidability and elimination of fixed point operators in the temporal logic USF. Technical report, Imperial College, 1989.

    Google Scholar 

  38. I. Hodkinson. Automata and temporal logic, forthcoming. chapter 2, in [Gabbav et al., 20001.

    Google Scholar 

  39. J. Hoperoft and J. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

    Google Scholar 

  40. H. Kamp. Seminar notes on tense logics. J. Symbolic Logic, 1968.

    Google Scholar 

  41. H. Kamp. Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles, 1968.

    Google Scholar 

  42. Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In A decade of concurrency: reflections and perspectives: REX school/symposium, Noordwijkerhout, the Netherlands, June 1–4, 1993, pages 273–346. Springer-Verlag, 1994.

    Google Scholar 

  43. S. Kleene. Representation of events in nerve nets and finite automata. In C. Shannon and J. McCarthy, editors, Automata Studies, pages 3–41. Princeton Univ. Press, 1956.

    Google Scholar 

  44. K. Konolige. A Deductive Model of Belief. Research notes in Artifiicial Intelligence. Morgan Kaufmann, 1986.

    Google Scholar 

  45. M. Kracht and F. Wolter. Properties of independently axiomatizable bimodal logics. Journal of Symbolic Logic, 56(4):1469–1485, 1991.

    Article  Google Scholar 

  46. S. Kuhn. The domino relation: flattening a two-dimensional logic. J. of Philosophical Logic, 18:173–195, 1989.

    Article  Google Scholar 

  47. H. Läuchli and J. Leonard. On the elementary theory of linear order. Fundamenta Mathematicae, 59:109–116, 1966.

    Google Scholar 

  48. O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In R. Parikh, editor, Logics of Programs (Proc. Conf. Brooklyn USA 1985), volume 193 of Lecture Notes in Computer Science, pages 196–218. Springer-Verlag, Berlin, 1985.

    Google Scholar 

  49. Z. Manna and A. Pnueli. The anchored version of the temporal framework. In REX Workshop, Noordwijkerh., 1988. LNCS 354.

    Google Scholar 

  50. M. Marx. Complexity of products of modal logics, Journal of Logic and Computation, 9:221–238, 1999.

    Google Scholar 

  51. M. Marx and M. Reynolds. Undecidability of compass logic. Journal of Looic and Computation, 9(6):897–914, 1999.

    Article  Google Scholar 

  52. M. Marx and Y. Venema. Multi Dimensional Modal Logic. Applied Logic Series No.4 Kluwer Academic Publishers, 1997.

    Book  Google Scholar 

  53. R. McNaughton. Testing and generating infinite sequences by finite automata. Information and Control, 9:521–530, 1966.

    Article  Google Scholar 

  54. D. Muller. Infinite sequences and finite machines. In Proceedings 4th Ann. IEEE Symp. on Switching Circuit Theory and Logical Design, pages 3–16, 1963.

    Chapter  Google Scholar 

  55. I. Németi. Decidable versions of first order logic and cylindric-relativized set algebras. In L. Csirmaz, D. Gabbay, and M. de Rijke, editors, Logic Colloquium’92, pages 171–241. CSLI Publications, 1995.

    Google Scholar 

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

    Article  Google Scholar 

  57. D. Perrin. Finite automata. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B. Elsevier, Amsterdam, 1990.

    Google Scholar 

  58. A. Pnueli. The temporal logic of programs. In Proceedings of the Eighteenth Symposium on Foundations of Computer Science, pages 46–57, 1977. Providence. RI.

    Google Scholar 

  59. A. Prior. Time and Modality. Oxford University Press, 1957.

    Google Scholar 

  60. M. Rabin and D. Scott. Finite automata and their decision problem. IBM J. of Res., 3:115–124, 1959.

    Google Scholar 

  61. M. O. Rabin. Decidability of second order theories and automata on infinite trees. American Mathematical Society Transactions, 141:1–35, 1969.

    Google Scholar 

  62. M. Rabin. Automata on Infinite Objects and Church’s Problem. Amer. Math. Soc., 1972.

    Google Scholar 

  63. A. Rabinovich. On the decidability of continuous time specification formalisms. Journal of Logic and Computation, 8:669–678, 1998.

    Article  Google Scholar 

  64. M. Reynolds and M. Zakharyaschev. On the products of linear modal logics. Journal of Logic and Computation, 6, 909–932, 2001.

    Article  Google Scholar 

  65. M. Reynolds. An axiomatization for Until and Since over the reals without the IRR rule. Studia Logica, 51:165–193, May 1992.

    Article  Google Scholar 

  66. M. Reynolds. Axiomatizing U and S over integer time. In D. Gabbay and H.-J. Ohlbach, editors, Temporal Logic, First International Conference, ICTL’94, Bonn, Germany, July 11–14, 1994, Proceedings, volume 827 of Lecture Notes in A.I., pages 117–132. Springer-Verlag, 1994.

    Google Scholar 

  67. M. Reynolds. A decidable logic of parallelism. Notre Dame Journal of Formal Logic, 38, 419–436, 1997.

    Article  Google Scholar 

  68. M. Reynolds. The complexity of the temporal logic with until over general linear time, submitted 1999. Draft version of manuscript available at http: //www.it.murdoch.edu.au/~mark/research/online/cult.html

    Google Scholar 

  69. E.L. Robertson. Structure of complexity in weak monadic second order theories of the natural numbers. In Proc. 6th Symp. on Theory of Computing, pages 161–171, 1974.

    Google Scholar 

  70. W. J. Savitch. Relationships between non-deterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4:177–192, 1970.

    Article  Google Scholar 

  71. R. Sherman, A. Pnueli, and D. Harel. Is the interesting part of process logic uninteresting: a translation from PL to PDL. SIAM J. on Computing, 13:825–839, 1984.

    Article  Google Scholar 

  72. A. Sistla and E. Clarke. Complexity of propositional linear temporal logics. J. ACM, 32:733–749, 1985.

    Article  Google Scholar 

  73. A. Sistla, M. Vardi, and P. Wolper. The complementation problem for Buchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.

    Article  Google Scholar 

  74. E. Spaan. Complexity of Modal Logics. PhD thesis, Free University of Amsterdam, Falculteit Wiskunde en Informatica, Universiteit van Amsterdam. 1993.

    Google Scholar 

  75. W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B. Elsevier, Amsterdam, 1990.

    Google Scholar 

  76. R. H. Thomason. Combinations of Tense and Modality. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume II, pages 135–165. D. Reidel Publishing Company, 1984. Reproduced in this volume.

    Chapter  Google Scholar 

  77. J. F. A. K. van Benthem. The logic of time. 2nd edition. Kluwer Academic Publishers, Dordrecht, 1991.

    Book  Google Scholar 

  78. J. van Benthem. Exploring Logical Dynamics. Cambridge University Press, 1996.

    Google Scholar 

  79. M. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115:1–37, 1994.

    Article  Google Scholar 

  80. Y. Venema. Expressiveness and Completeness of an Interval Tense Logic. Notre Dame Journal of Formal Logic, 31(4), Fall 1990.

    Article  Google Scholar 

  81. Y. Venema. Completeness via completeness. In M. de Rijke, editor, Colloquium on Modal Logic, 1991. ITLI-Network Publication, Instit. for Lang., Logic and Information, University of Amsterdam, 1991.

    Google Scholar 

  82. Y. Venema. Derivation rules as anti-axioms in modal logic. Journal of Symbolic Logic, 58:1003–1034, 1993.

    Article  Google Scholar 

  83. P. Wolper. Temporal logic can be more expressive. Information and computation, 56(1–2):72–99, 1983.

    Google Scholar 

  84. Ming Xu. On some U, S-tense logics. J. of Philosophical Logic, 17:181–202, 1988.

    Google Scholar 

  85. A. Zanardo. A complete deductive system for since-until branching time logic. J. Philosophical Logic, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Ciência da Computação, University of Sao Paulo, Brazil

    M. Finger

  2. Department of Computer Science, King’s College, London, UK

    D. Gabbay

  3. School of Information Technology, Murdoch University, Australia

    M. Reynolds

Authors
  1. M. Finger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. D. Gabbay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. M. Reynolds
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. King’s College, London, UK

    D. M. Gabbay

  2. Centrum für Informations- und Sprachverarbeitung, Ludwig-Maximilians-Universität München, Germany

    F. Guenthner

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer Science+Business Media Dordrecht

About this chapter

Cite this chapter

Finger, M., Gabbay, D., Reynolds, M. (2002). Advanced Tense Logic. In: Gabbay, D.M., Guenthner, F. (eds) Handbook of Philosophical Logic. Handbook of Philosophical Logic, vol 7. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0462-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-94-017-0462-5_2

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-90-481-6011-2

  • Online ISBN: 978-94-017-0462-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation