Abstract
We consider a first order timed logic that is an extension of the theory of real addition and scalar multiplications (by rational numbers) by unary functions and predicates of time. The time is treated as non negative reals. This logic seems to be well adapted to a direct, full-scale specification of real-time systems. It also suffices to describe runs of timed algorithms that have as inputs functions of time. Thus it permits to embed the verification of timed systems in one easily understandable framework. But this logic is incomplete, and hence undecidable. To develop an algorithmic support for the verification problem one theoretical direction of research is to look for reasonable decidable classes of the verification problem. In this paper we describe such classes modeling typical properties of practical systems such as dependence of behavior only on a small piece of history and periodicity.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, T. Henzinger, and P.-H. Ho. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, editors, Workshop on Theory of Hybrid Systems, 1992, pages 209–229. Springer Verlag, 1993. Lect. Notes in Comput. Sci, vol. 736.
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
D. Beauquier and A. Slissenko. On semantics of algorithms with continuous time. Technical Report 97-15, Revised version., University Paris 12, Department of Informatics, 1997. Available at http://www.eecs.umich.edu/gasm/ and at http://www.univ-paris12.fr/lacl/.
D. Beauquier and A. Slissenko. The railroad crossing problem: Towards semantics of timed algorithms and their model-checking in high-level languages. In M. Bidoit and M. Dauchet, editors, TAPSOFT’97: Theory and Practice of Software Development, pages 201–212. Springer Verlag, 1997. Lect. Notes in Comput. Sci., vol. 1214.
D. Beauquier and A. Slissenko. Decidable verification for reducible timed automata specified in a first order logic with time. Technical Report 98-16, University Paris 12, Department of Informatics, 1998. Available at http://www.univparis12.fr/lacl/.
A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Vol. B: Formal Models and Sematics, pages 995–1072. Elsevier Science Publishers B.V., 1990.
Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods, pages 9–93. Oxford University Press, 1995.
H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. Elsevier, 1994. Series: “Real Time Safety Critical System”, vol. 1. Series Editor: H. Zedan.
T. Henzinger. It’s about time: real-time logics reviewed. In Proc. 10th CONCUR, pages 439–454. Springer-Verlag, 1998. Lect. Notes in Comput. Sci., vol. 1466.
Y. Hirshfeld and A. Rabinovich. Quantitative temporal logic. Manuscript, 11 p., 1998.
Y. Hirshfeld and A. Rabinovich. A framework for decidable metrical logics. Manuscript, 13 p., 1999.
PVS. PVS. WWW site of PVS papers. http://www.csl.sri.com/sri-csl-fm.html.
A. Rabinovich. Decidability in monadic logic of order over finitely variable signals. Manuscript, 15 p., 1997.
A. Rabinovich. On the decidability of continuous time specification formalisms. Manuscript, 15 p., 1997. To appear in J. of Logic and Comput.
A. Rabinovich. Expressive completeness of duration calculus. Manuscript, 33 p., 1998.
B. Trakhtenbrot. Automata and hybrid systems. Lecture Notes 153, Uppsala University, Computing Science Department, 1998. Edited by F. Moller and B. Trakhtenbrot.
V. Weispfenning. Mixed real-integer linear quantifier elimination. In Proc. of the 1999 Int. Symp. on Symbolic and Algebraic Computations (ISSAC’99), ACM Press, 1999. To appear.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beauquier, D., Slissenko, A. (1999). Decidable classes of the verification problem in a timed predicate logic. In: Ciobanu, G., Păun, G. (eds) Fundamentals of Computation Theory. FCT 1999. Lecture Notes in Computer Science, vol 1684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48321-7_7
Download citation
DOI: https://doi.org/10.1007/3-540-48321-7_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66412-3
Online ISBN: 978-3-540-48321-2
eBook Packages: Springer Book Archive