Abstract
In this paper we study two possible semantics for the real-time logic MTL (Metric Temporal Logic). In the first semantics, called dense time semantics, time is modeled by the positive real numbers. In the second one, called fictitious clock semantics, real-time information is delivered by a global fictitious clock. We show that the fictitious clock semantics can be viewed as an abstraction of the dense time semantics. This abstraction relation is formalized by a parametric conservative connection. This formalization can be used to partially decide undecidable problems in the dense time semantics by reasoning on the fictitious clock semantics.
Chapter PDF
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
R. Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University, 1991.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 414–425, Philadelphia, June 1990.
R. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 74–106. Springer-Verlag, 1992.
R. Alur and T.A. Henzinger. Real-time logics: complexity and expressiveness. Information and Computation, 104(1):35–77, 1993. Preliminary version appears in the Proc. of 5th LICS, 1990.
R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–204, 1994. Preliminary version appears in Proc. 30th FOCS, 1989.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 428–439, Philadelphia, June 1990.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of Fourth ACM Symposium on Programming Languages (POPL'77), pages 238–252, Los Angeles, California, January 1977.
P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.
P. Cousot and R. Cousot. Comparison of the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation (Invited Paper). In M. Bruynooghe and M. Wirsing, editors, Proceedings of the Fourth International Workshop on Programming Language Implementation and Logic Programming (PLILP'92), Lecture Notes in Computer Science, Leuven, August 1992. Springer-Verlag.
E.A. Emerson. Handbook in Theoretical Computer Science, Formal Models and Semantics, chapter Temporal and Modal Logic, pages 995–1072. Elsevier, 1990.
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.
T.A. Henzinger, Z. Manna, and A. Pnueli. What good are digital clocks? In W. Kuich, editor, ICALP 92: Automata, Languages, and Programming, Lecture Notes in Computer Science 623, pages 545–558. Springer-Verlag, 1992.
Ron Koymans. Specifying message passing and time-critical systems with temporal logic. LNCS 651, Springer-Verlag, 1992.
A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46–57, 1977.
J.-F. Raskin. Model-Generation of a Fictitious Clock Real-Time Logic: A Symbolic Decision Procedure Using Sharing-Trees. Research Paper RP-09-96, Computer Science Department, FUNDP, Namur (Belgium), March 1996.
J.-F. Raskin and P.-Y. Schobbens. Real-Time Logics: Fictitious Clock as an Abstraction of Dense Time. Research Paper RP-17-96, Computer Science Department, FUNDP, Namur (Belgium), September 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Raskin, JF., Schobbens, PY. (1997). Real-time logics: Fictitious clock as an abstraction of dense time. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035387
Download citation
DOI: https://doi.org/10.1007/BFb0035387
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive