Decidable classes of the verification problem in a timed predicate logic
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.
KeywordsTemporal Logic Atomic Formula Hybrid Automaton Decidable Classis Abstract State Machine
Unable to display preview. Download preview PDF.
- ACHH93.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.Google Scholar
- BS97b.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.Google Scholar
- BS98.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/.
- Eme90.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.Google Scholar
- Gur95.Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. Börger, editor, Specification and Validation Methods, pages 9–93. Oxford University Press, 1995.Google Scholar
- Han94.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.Google Scholar
- Hen98.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.Google Scholar
- HR98.Y. Hirshfeld and A. Rabinovich. Quantitative temporal logic. Manuscript, 11 p., 1998.Google Scholar
- HR99.Y. Hirshfeld and A. Rabinovich. A framework for decidable metrical logics. Manuscript, 13 p., 1999.Google Scholar
- PVS. PVS. WWW site of PVS papers. http://www.csl.sri.com/sri-csl-fm.html.
- Rab97a.A. Rabinovich. Decidability in monadic logic of order over finitely variable signals. Manuscript, 15 p., 1997.Google Scholar
- Rab97b.A. Rabinovich. On the decidability of continuous time specification formalisms. Manuscript, 15 p., 1997. To appear in J. of Logic and Comput.Google Scholar
- Rab98.A. Rabinovich. Expressive completeness of duration calculus. Manuscript, 33 p., 1998.Google Scholar
- Tra98.B. Trakhtenbrot. Automata and hybrid systems. Lecture Notes 153, Uppsala University, Computing Science Department, 1998. Edited by F. Moller and B. Trakhtenbrot.Google Scholar
- Wei99.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.Google Scholar