Grande Salle de VERIMAG
10 May 2010 - 16h30
Verification of quantitative properties on constraint automata
by Regis Gascon from Inria Sophia-Antipolis
Abstract: Traditional temporal logics like LTL or CTL* use propositional variables
as atomic formulas.
Consequently, these logics allow only to state properties on the control
locations of the models.
They are not well suited to state richer properties on the objects
(data) that models can handle:
intergers (counters), reals (clocks), strings (stacks, queues)...
Indeed, this kind of
data are interpreted in infinite domains so they cannot be encoded with
propositinal variables.
We have introduced a general definition for extensing of temporal logics
with constraints
induced by a concrete domain, i.e. an (infinite) interpretation domain
and a set of relations. These
extensions also allow to compare values of the variables at different
states of an execution.
I will mainly consider temporal logics extended with constraints on
counters induced by Presburger
arithmetic. These logics allows to state properties on counter automata
which is a ubiquitous model in
verification. Unfortunately, problems for counter automata are often
undecidable. I will study several
restrictions on the set of constraints allowed and/or the syntactic
ressources of the models (number of
variables, capability of comparing variables different states). The goal
is to identify the kind of
restrictions that allows to regain decidabilty. The techniques used to
establish these results are automata
constructions combining some usual constructions with finite
abstraction methods for infinite datas.
