Abstract
We claim in this paper that the Propositional Temporal Logic (PTL) is an adequate logic to specify a reactive system. To prove this affirmation, we present abbreviations which allow the expression of the most important real-time properties and some other important requirements. We show that they are easy to use and that the induced complexity cost is the same as the complexity of the other real-time logics. Finally, we prove that many real-time logics already published have exactly the same expressive power as PTL.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur and T. A. Henzinger A really temporal logic IEEE Symp. on Found. of Comp. Sci., pages 164–169, 1989.
R. Alur and T. A. Henzinger Real-time logics: complexity and expressiveness IEEE Logic in Comp. Sci., pages 390–401, 1990.
R. Alur, C. Courcoubetis and D. Dill Model-checking for real-time systems IEEE Logic in Comp. Sci., pages 414–425, 1990.
E. A. Emerson and J. Y. Halpern “Sometimes” and “not never” revisited: on branching versus linear time temporal logic Journal of the ACM, 33(1):151–178, January 1986.
E. Harel, O. Lichtenstein, and A. Pnueli Explicit clock temporal logic IEEE Logic in Comp. Sci., pages 402–413, 1990.
T. A. Henzinger, Z. Manna and A. Pnueli Temporal proof methodologies for real-time systems ACM Princ. of Distr. Comp., pages 353–366, 1990.
F. Jahanian and A. K. Mok Safety analysis of timing properties in real-time systems IEEE Trans. on Software Engineering, 12(9):890–904, September 1986.
R. Koymans Specifying real-time properties with metric temporal logic Journal of Real-Time Systems, 1(2):255–299, 1990.
H. Lewis A logic of concrete time intervals IEEE Logic in Comp. Sci., pages 414–425, 1990.
Z. Manna and A. Pnueli A hierarchy of temporal properties ACM Princ. of Distr. Comp., pages 353–366, 1990.
J. S. Ostroff Real-time temporal logic decision procedures IEEE Real Time Syst. Symp., pages 92–101, 1989.
D. Pilaud and N. Halbwachs From a synchronous declarative language to a temporal logic dealing with multiform time Formal Techniques in Real-Time and Fault-Tolerant Systems 1988, LNCS 331, pages 99–110, 1988.
A. Pnueli and E. Harel Applications of temporal logic to the specification of real-time systems Formal Techniques in Real-Time and Fault-Tolerant Systems 1988, LNCS 331, pages 84–98, 1988.
A. P. Sistla and E. M. Clarke The complexity of propositional linear temporal logics Journal of the ACM, 32(3):733–749, July 1985.
P. Wolper Temporal logic can be more expressive Information and Control, (56):72–99, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nassor, E., Vidal-Naquet, G. (1992). Suitability of the propositional temporal logic to express properties of real-time systems. In: Finkel, A., Jantzen, M. (eds) STACS 92. STACS 1992. Lecture Notes in Computer Science, vol 577. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55210-3_173
Download citation
DOI: https://doi.org/10.1007/3-540-55210-3_173
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55210-9
Online ISBN: 978-3-540-46775-5
eBook Packages: Springer Book Archive