Abstract
Kamp’s theorem established the expressive completeness of the temporal modalities Until and Since for the First-Order Monadic Logic of Order (FOMLO) over Real and Natural time flows. Over Natural time, a single future modality (Until) is sufficient to express all future FOMLO formulas. These are formulas whose truth value at any moment is determined by what happens from that moment on. Yet this fails to extend to Real time domains: Here no finite basis of future modalities can express all future FOMLO formulas. In this paper we show that finiteness can be recovered if we slightly soften the requirement that future formulas must be totally past-independent: We allow formulas to depend just on the very very near-past, and maintain the requirement that they be independent of the rest - actually - of most of the past. We call them ‘almost future’ formulas, and show that there is a finite basis of almost future modalities which is expressively complete over the Reals for the almost future fragment of FOMLO.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Formal Logic 26(2), 115–128 (1985)
Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal logic: Mathematical Foundations and Computational Aspects. Oxford University Press (1994)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the Temporal Analysis of Fairness. In: POPL 1980, pp. 163–173 (1980)
Hirshfeld, Y., Rabinovich, A.: Future temporal logic needs infinitely many modalities. Information and Computation 187, 196–208 (2003)
Hodkinson, I.: Notes on games in temporal logic. Lecture Notes for LUATCS Meting, Johannesburg (December 1999), http://www.doc.ic.ac.uk/~imh/index.html
Kamp, H.W.: Tense logic and the theory of linear order. Phd thesis, University of California, Los Angeles (1968)
Pnueli, A.: The temporal logic of programs. In: Proc. IEEE 18th Annu. Symp. on Found. Comput. Sci., pp. 46–57. IEEE, New York (1977)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pardo (Ordentlich), D., Rabinovich, A. (2012). A Finite Basis for ‘Almost Future’ Temporal Logic over the Reals. In: Rovan, B., Sassone, V., Widmayer, P. (eds) Mathematical Foundations of Computer Science 2012. MFCS 2012. Lecture Notes in Computer Science, vol 7464. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32589-2_64
Download citation
DOI: https://doi.org/10.1007/978-3-642-32589-2_64
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32588-5
Online ISBN: 978-3-642-32589-2
eBook Packages: Computer ScienceComputer Science (R0)