Advertisement

Verification in Predicate Logic with Time: Algorithmic Questions

  • Anatol Slissenko
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)

Abstract

We discuss the verification of timed systems within predicate logics with explicit time and arithmetical operations. The main problem is to find efficient algorithms to treat practical problems. One way is to find practically decidable classes that englobe this or that class of practical problems. This is our main goal, where we concentrate on one approach that permits to arrive at a kind of small model property. We will also touch the question of extension of these results to probabilistic systems that will be presented in more detail elsewhere.

Keywords

Model Check Arithmetical Operation Predicate Logic Decidable Classis Bound Model Check 
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. 1.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Beauquier, D., Crolard, T., Prokofieva, E.: Automatic verification of real time systems: A case study. In: Third Workshop on Automated Verification of Critical Systems (AVoCS 2003), University of Southampton, pp. 98–108 (2003)Google Scholar
  3. 3.
    Beauquier, D., Crolard, T., Prokofieva, E.: Automatic parametric verification of a root contention protocol based on abstract state machines and first order timed logic. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 372–387. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Beauquier, D., Crolard, T., Slissenko, A.: A predicate logic framework for mechanical verification of real-time Gurevich Abstract State Machines: A case study with PVS. Technical Report 00–25, University Paris 12, Department of Informatics (2000), Available at http://www.univ-paris12.fr/lacl/
  5. 5.
    Beauquier, D., Rabinovich, A., Slissenko, A.: A logic of probability with decidable model-checking. Journal of Logic and Computation, 24 pages (to appear)Google Scholar
  6. 6.
    Beauquier, D., Slissenko, A.: Periodicity based decidable classes in a first order timed logic. Annals of Pure and Applied Logic, 38 pages (to appear)Google Scholar
  7. 7.
    Beauquier, D., Slissenko, A.: Decidable verification for reducible timed automata specified in a first order logic with time. Theoretical Computer Science 275(1-2), 347–388 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Beauquier, D., Slissenko, A.: A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic 113(1-3), 13–52 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: An overview. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 1–19. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85–96. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Fagin, R., Halpern, J.: Reasoning about knowledge and probability. J. of the Assoc. Comput. Mach. 41(2), 340–367 (1994)zbMATHMathSciNetGoogle Scholar
  12. 12.
    Gurevich, Y., Huggins, J.: The railroad crossing problem: an experiment with instantaneous actions and immediate reactions. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 266–290. Springer, Heidelberg (1996)Google Scholar
  13. 13.
    Halpern, J.: Presburger arithmetic with unary predicates is π1 1-complete. J. of symbolic Logic 56, 637–642 (1991)zbMATHCrossRefGoogle Scholar
  14. 14.
    Sanders, J., Curran, E.: Software Quality. Addison-Wesley, Reading (1994)Google Scholar
  15. 15.
    Slissenko, A.: A logic framework for verification of timed algorithms. Fundamenta Informaticae 69, 1–39 (2004)MathSciNetGoogle Scholar
  16. 16.
    Sommerville, I.: Software Engineering, 4th edn. Addison-Wesley, Reading (1992)Google Scholar
  17. 17.
    Sorea, M.: Bounded model checking for timed automata. Electronic Notes in Theoretical Computer Science 68(5) (2002), http://www.elsevier.com/locate/entcs/volume68.html
  18. 18.
    Tel, G. (ed.): Introduction to Distributed Algorithms. Cambridge University Press, Cambridge (1994)zbMATHGoogle Scholar
  19. 19.
    Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: Proc. of the 1999 Int. Symp. on Symbolic and Algebraic Computations (ISSAC 1999), pp. 129–136. ACM Press, New York (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Anatol Slissenko
    • 1
    • 2
  1. 1.Laboratory for AlgorithmicsComplexity and Logic, University Paris-1France
  2. 2.Dept. of InformaticsUniversity Paris-12CréteilFrance

Personalised recommendations