Verification in Predicate Logic with Time: Algorithmic Questions
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.
KeywordsModel Check Arithmetical Operation Predicate Logic Decidable Classis Bound Model Check
Unable to display preview. Download preview PDF.
- 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
- 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.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.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
- 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
- 14.Sanders, J., Curran, E.: Software Quality. Addison-Wesley, Reading (1994)Google Scholar
- 16.Sommerville, I.: Software Engineering, 4th edn. Addison-Wesley, Reading (1992)Google Scholar
- 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