Advertisement

Decidable classes of the verification problem in a timed predicate logic

  • Danièle Beauquier
  • Anatol Slissenko
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)

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.

Keywords

Temporal Logic Atomic Formula Hybrid Automaton Decidable Classis Abstract State Machine 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. AD94.
    R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  3. BS97a.
    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/.
  4. 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
  5. 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/.
  6. 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
  7. 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
  8. 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
  9. 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
  10. HR98.
    Y. Hirshfeld and A. Rabinovich. Quantitative temporal logic. Manuscript, 11 p., 1998.Google Scholar
  11. HR99.
    Y. Hirshfeld and A. Rabinovich. A framework for decidable metrical logics. Manuscript, 13 p., 1999.Google Scholar
  12. PVS. PVS. WWW site of PVS papers. http://www.csl.sri.com/sri-csl-fm.html.
  13. Rab97a.
    A. Rabinovich. Decidability in monadic logic of order over finitely variable signals. Manuscript, 15 p., 1997.Google Scholar
  14. 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
  15. Rab98.
    A. Rabinovich. Expressive completeness of duration calculus. Manuscript, 33 p., 1998.Google Scholar
  16. 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
  17. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Danièle Beauquier
    • 1
  • Anatol Slissenko
    • 1
  1. 1.Dept. of InformaticsUniversity Paris-12CrèteilFrance

Personalised recommendations