*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.