Abstract
The connection between temporal logic, first-order logic and formal language theory is well known in the context of propositional temporal logic (PTL). In the present paper the situation is analyzed for the propositional interval temporal logic (ITL), which has been used for the specification of digital circuits. In contrast to PTL the propositional variables of ITL formulas are interpreted in sequences of states (intervals) instead of a single state. This motivates a calculus of star-free regular expressions with a new interpretation of the basic constants (by words instead of letters). We will show here that ITL is strictly more expressive than this calculus of star-free expressions, but strictly less expressive than a corresponding first-order language. For the proof we use a modification of the Ehrenfeucht-Fraissé games, capturing the expressive power of the extended star-free expressions.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
D. Gabbay, A. Pnueli, S. Shelah, J. Stavi, On the temporal analysis of fairness, 7th ACM Symp. on Principles of Progr. Languages (1980), 163–173.
H.W. Kamp, Tense logic and the theory of linear order, Ph.D. Thesis, Univ. of California, Los Angeles (1968).
R.E. Lander, Application of model-theoretic games to the theory of linear orders and finite automata, Inf. Contr. 33 (1977), 281–303.
D. Lippert, W. Thomas, Relativized star-free expressions, first-order logic, and a concatenation game, Springer Lecture Notes of Mathematics 1320 (1988), 194–204.
D. Lippert, Ausdrucksstärke der Intervall-Temporallogik: Eine Untersuchung mit spieltheoretischen Methoden. Diplomarbeit, RWTH Aachen 1986.
B.C. Moszkowski, Reasoning about digital circuits, PhD Dissertation, Stanford University 1983.
B. Moszkowski, Z. Manna, Reasoning in interval temporal logic, In: Logic of Programs (E. Clarke, D. Kozen, Eds.), Springer Lecture Notes in Computer Science 164 (1984), 371–384.
R. McNaughton, S. Papert, Counter-Free Automata, MIT Press, Cambridge, Mass. 1971.
Z. Manna, A. Pnueli, Verification of concurrent programs: the temporal framework, in: The Correctness Problem in Computer Science (eds. R.S. Boyer, J.S. Moore), Int. Lect. Series in Comp. Sci., Academic Press (1981)
A. Pnueli, The temporal logic of programs, Proc. 18th IEEE Symp. Found. of Comput. Sci. (Providence, R.I.), (1977), 46–57.
J.G. Rosenstein, Linear Orderings, Academic Press, New York (1982).
W. Thomas, Classifying regular events in symbolic logic, J. Comput. System Sci. 25 (1982), 360–376.
W. Thomas, An application of the Ehrenfeucht-Fraissé game in formal language theory, Mem. Soc. Math. France 16 (1984), 11–21.
L. Zuck, Past Temporal Logic, Ph.D. Thesis, The Weizmann Institute of Science, Rehovot, Israel (1986).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lippert, D. (1989). Interval temporal logic and star-free expressions. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '88. CSL 1988. Lecture Notes in Computer Science, vol 385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026302
Download citation
DOI: https://doi.org/10.1007/BFb0026302
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51659-0
Online ISBN: 978-3-540-46736-6
eBook Packages: Springer Book Archive