A Logic for Specification of Timed Algorithms
by
Anatol Slissenko
University Paris 12
Coauthors: D. Beauquier

By the verification problem we mean here the problem of verifying whether a given high-level program specification satisfies a given requirements specification. In the context of the verification problem it is presumed that the requirement specification is declarative and describes the desired properties without relating them to their algorithmic realization. As for the high-level program specification it is presumed to give main lines of realization without going into secondary details and, in fact, in a machine independent manner.

Though the passage from a requirements specification to a high-level program specification is often a source of grave and hard to detect errors, the analysis of this passage is not a popular topic in the verification literature. We consider systems with explicit time constraints that are also called real-time systems. The time is continuous and is modeled by reals. Our main goal is to analyze how one can represent the verification problem in a first order applied logic, being given a requirements specification in a natural language and a program specification in an abstract state machine language with a clear intuitive semantics. So no particular languages are imposed, and easy understandability and expressibility of the used formalisms consitute a crucial point of our treatment.

To specify programs we consider abstract state machines (here that of Y. Gurevich) as they are easy to understand, in particular, from the point of view of their semantics. They are based on traditional logical notions and that makes them attractive. As a language for requirements specifications we consider one type of first order timed logic (FOTL) with explicit continuous time as we started earlier and discuss its monadic second order extension. A FOTL is an extension of a decidable theory of reals, e. g. of the theory of real addition, by unary timed functions and predicates. Such a logic is sufficiently expressive to permit to rewrite directly in its syntax the phrases of a natural language concerning a requirements specification of a timed system.

We consider continuous time as it is usually used in specifications of, say, hybrid systems. FOTL permits to express numerous properties that appear in such specifications and are not treatable within traditionally used temporal logics. For example, the property "two x-events are never separated by exactly 1 time unit" can be directly rewritten as the FOTL formula    not existstt' (x(t) /\ x(t') /\ |t-t'|=1). Another example, the property "the average value of the clocks x₁, ..., x_n does not exceed d" can be directly rewritten as the formula    for allt (x₁(t)+...+x_n(t) <= n·d)   with t being a time variable, and moreover one can treat n and d as abstract constants. The availability of arithmetics permits to easily specify also such problems as clock synchronization that is impossible for commonly used temporal logics. And we have in fact only one logic to consider, as compared with numerous temporal logics.

For abstract state machines with continuous time we define its semantics, i. e. the set of its runs, and show that this set can be represented by a formula of FOTL. The examples show that proofs of correctness of algorithms within this framework are short, clear and based on heuristics that may be not hard to extract as strategies of proof search. Remark that our analysis of the widely studied Generalized Railroad Crossing Problem found an error in the paper of C. Heitmeyer and N. Lynch who introduced the problem, and in some other papers who repeated this error.

Sure, FOTL is incomplete and thus undecidable. However, we can describe semantically some decidable classes that contain specifications of systems with "finite memory". This property is rather typical for practical systems of control. The decidability is based on the fact that the underlying theory of FOTL, that is, say, the theory of real addition is decidable.

The verification problem can be treated as establishing the validity of some proposition (\Phi_Prg --> \Phi_Rqmt) expressing that all the runs defined by a program specification and described by a formula \Phi_Prg meet the requirements specification described by a formula \Phi_Rqmt. We introduce two notions which model different "finiteness" properties of timed systems. These notions are formulated in terms of formula interpretations and are called finite satisfiability and local refutability. Finite satisfiability of a formula \Phi says that every "finite piece" of any model of \Phi is extendable to a "finite" model of \Phi. Local refutability says that if a formula is refutable, i. e. possesses a counter-model, the contradiction given by this counter-model is concentrated on a finite piece of a fixed size; and it is so for every counter-model. We prove that the class of implications of our logic where the premise is finitely satisfiable with a fixed complexity and the conclusion is locally refutable (again with a given complexity) is decidable. Thus, we have a decidable class of verification problems of the form (\Phi_Prg --> \Phi_Rqmt), where \Phi_Prg is finitely satisfiable and \Phi_Rqmt is locally refutable (with a fixed complexity).

Clearly, the finiteness properties are undecidable in the general case. In the examples we looked at, the local refutability of requirements of functioning is easy to check, but to find interesting decidable sufficient conditions for it rests an open problem. Concerning finite satisfiability, we analysed in another paper its connection with the property of algorithms that can be described as "reducibility". For timed automata considered as program description that gives decidable finite satisfiability. More precisely, the formula representing the runs of a reducible timed automaton is finitely satisfiable, and the reducibility is decidable.

The mentioned considerations concerning the decidability based on the finiteness properties work for the monadic second order timed logic that permits to express some important properties related to the verification problem that are out of the scope of FOTL.

Preliminary texts concerning the mentioned results are available at
http://www.univ-paris12.fr/lacl/ as TR-97-15 and TR-98-16.

Date received: March 1, 1999

Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-10.