A Logic Framework for Verification of Timed Algorithms

Issue title: Continuous Time Paradigms in Logic and Automata

Article type: Research Article

Authors: Slissenko, Anatol

Affiliations: Dept. of Informatics, University Paris-12, 61 Av. du Gén. de Gaulle, 94010, Créteil, France

Abstract: This paper is a survey of research of my colleagues and myself aimed at developing a comprehensive logical framework for the verification of real-time distributed systems. The framework is based on predicate logics with explicit time. To choose such a logic we pursue two goals: first, to make formalization of verification problems rather direct, without unjustified simplifications, and second, to have a logic which permits to describe decidable classes of the verifications problem covering the particular problems we are interested in. Notice that our intention is not to introduce new specification languages, but work directly with those of the user. In this paper we describe First Order Timed Logic (FOTL) that is sufficient to express the main part of verification of systems without uncertainty. The time is continuous (the formalism work as well for discrete time — in our context this case is less interesting and less efficient from algorithmic viewpoint). We give examples of problems that can be treated, describe how to represent runs of programs in FOTL, introduce decidable classes, discuss aspects of practical efficiency. We conclude with open questions.

Journal: Fundamenta Informaticae, vol. 62, no. 1, pp. 29-67, 2004