5 juin 2003 |
Erich Grädel
Once upon a time, two players set out on an infinite ride through the
west. More often than not, they had quite different ideas on where to
go, but for reasons that have by now been forgotten they were forced
to stay together -- as long as they were both alive.
They agreed on the rule that each player can determine on every second
day, where the ride should go. After omega days, an infinite ride is
completed and it is time for payoff.
There were variants of this game where, after some number of days,
one of the players would be eliminated (these things happened in the west)
and the other was to complete the game by himself for the remaining
omega days (a very lonesome ride, indeed).
Path games arise also in other contexts than the wild west. They have been studied in descriptive set theory, in the form of Banach-Mazur games, which are path games on the infinite omega-branching tree. An important issue in this context is determinacy (does one of the players have a winning strategy?) and its dependency on the topological properties of the winning condition. In a quite different setting, Pistore and Vardi have recently used path games for task planning in nondeterministic domains. Rather than determinacy (which is obvious for winning conditions in such applications), the main concern here are the algorithmic properties. It turns out that planning problems modeled by path games can be solved by automata-based methods. Here we consider path games in a general, abstract setting, but with emphasis on definability and complexity issues. After a brief review of the classical results on determinacy of Banach-Mazur games, we discuss path games that are positionally determined, i.e., admit winning strategies that only depend on the current position, not on the history of the play. This will be used to determine the complexity of deciding the winner of path games with LTL winning conditions. Finally we will investigate definability issues. We are interested in the question how the logical complexity of defining a winning condition (a property of infinite paths) is related to the logical complexity of defining who wins the associated game (a property of game graphs). In particular, we will see that the winner of path games with LTL winning conditions is definable in CTL$^*$. This is joint work with Dietmar Berwanger and Stephan Kreutzer. |
||||||
24 avril 2003 |
Stéphane Riedweg
Par extension des logiques temporelles, je propose un cadre formel et unifié pour une large classe de problèmes de contrôle. Cette extension est obtenue par quantification des proposition atomiques.
En particulier, une telle extension pour le mu-calcul est considérée et permet de spécifier, par exemple, des critères d'optimalité du contrôle comme la permissivité maximale. Elle ne permet cependant pas le contrôle sous observation partielle. Pour cela, une version quantifié du loop-mu-calculus est proposée et permet, dans le cadre [AVW03] (Arnold,Vincent, Walukiewicz: Games for synthesis of controllers with partial observation), de synthétiser un contrôleur maximal permissif parmi les contrôleurs sous observation partielle, par exemple. |
||||||
10 avril 2003 |
Catalin Dima
|
||||||
27 mars 2003 |
Richard Castanet
|
||||||
20 mars 2003 |
Mirabelle Nebut
L'approche synchrone est dédiée à la conception des systèmes réactifs.
Grâce à leur sémantique forte, des langages synchrones comme Esterel, Lustre et Signal permettent de spécifier le comportement des systèmes de manière abstraite et rendent possible leur validation formelle, cruciale dans le cas des systèmes critiques.
L'application aux programmes synchrones des méthodes de vérification concernant les systèmes infinis et les aspects numériques est fondamentale, mais plus ou moins directe. En effet l'utilisation d'horloges dans les spécifications donne aux variables un statut d'absence ou de présence. Dans le cas de Signal l'absence de variables est explicitée par une valeur spéciale, ce qui empèche l'interfaçage direct des outils aux techniques existantes. L'exposé traitera de la manipulation de l'absence des variables synchrones, plus particulièrement dans les langages flot de données. Après une introduction au paradigme synchrone et à l'utilisation des horloges, on donnera un état de l'art du traitement de l'absence dans les sémantiques et les analyses synchrones. Ensuite on présentera un langage logique d'horloges appelé CL, basé sur une extension par des aspects numériques des horloges booléennes utilisées dans le contexte de la compilation Signal. On montrera que CL permet d'interfacer naturellement les modèles étendus avec l'absence explicite à des théories standard, de plusieurs manières. |
||||||
13 mars 2003 |
Franck Pommereau
Cet exposé porte sur des modèles explicitant la concurrence
qui s'appliquent au domaine du temps-réel. Le point de départ
est un modèle basé sur des réseaux de Petri colorés
composables à la manière des termes dans les algèbres de
processus.
Nous montrons comment introduire dans ce cadre une représentation du temps, appelée « temps causal », dont l'originalité consiste à utiliser l'expressivité du modèle pour représenter explicitement une horloge dans les systèmes à temporiser. Cette approche se révèle souple et agréable à utiliser ; de plus, les résultats pratiques sont prometteurs puisqu'il a été possible de vérifier automatiquement des systèmes ainsi modélisés avec de meilleures performances que des méthodes réputées (les automates temporisés avec les outils UPPAAL et Kronos). Par ailleurs, nous montrons comment étendre le modèle de départ pour y introduire des opérateurs permettant de représenter la préemption, c'est-à-dire l'interruption définitive ou temporaire des processus d'un système. La seconde partie de l'exposé présente les bases formelles sur lesquelles s'appuient les travaux ci-dessus. Il s'agit d'algèbres de processus dotées de la structure suivante : une algèbre de termes est munie d'une sémantique opérationnelle au moyen de règles SOS ; une algèbre de réseaux de Petri permet de donner aux termes une sémantiques dénotationnelle ; ces deux sémantiques sont prouvées cohérentes (elles définissent les mêmes évolutions). |
||||||
6 mars 2003 |
Pierre Courtieu
La plate-forme Javacard est l'environnement pour la programmation des
cartes à puces de nouvelle génération. Elle intègre (entre autre) sur
une carte à puce les composants suivants: une machine virtuelle de
type Java(Card) (JCVM), un vérificateur de bytecode (BCV). Le rôle du
BCV est d'effectuer une analyse statique des programmes compilés en
bytecode devant être charger sur la puce, et d'autoriser ou non ce
chargement en fonction du résultat de cette analyse. L'analyse vérifie
plusieurs propriétés:
(*) en commun avec Gilles Barthe, Guillaume Dufay et Simao Melo De Sousa |
||||||
27 février 2003 |
Tayssir Touili
We consider the verification problem of programs with
unbounded (1) recursive procedure calls, and
(2) dynamic creation of concurrent processes.
Programs are modeled using term rewrite systems called PRS (for process
rewrite systems).
These models are more powerful than pushdown automata and Petri nets,
two common models for reasoning about, respectively,
recursive programs without process creation, and
multi-threaded programs without recursive calls.
A PRS can actually be seen as the nesting of
prefix rewrite system and a multiset rewrite system.
We define a generic procedure which constructs a finite representation of the set of all reachable configurations of a given PRS, provided that its underlying multiset rewrite system is semilinear. We represent PRS reachability sets by means of a new class of tree automata with unbounded width. Our procedure can be instantiated in different ways leading to new reachability analysis procedures for PRS. (Joint work with Ahmed Bouajjani) |
||||||
13 février 2003 |
Sabine Pérès
Le langage formel CTL permet d'exprimer dans une logique modale des
propriétés d'un réseau de régulation génétique. Le système
biologique choisi pour illustrer l'utilisation de ce langage formel est
la production de mucus dans Pseudomonas aeruginosa, une
bactérie mucoïde jouant un rôle important dans la mucoviscidose. Des
biologistes de Rouen ont émis l'hypothèse que la production de
mucus de cette bactérie était un phénomène épigénétique et ont proposé
un ensemble de modèles. Les réseaux de régulation
multivalués développés par René Thomas qui permettent d'étudier ce type
de système, constituent la sémantique de cette approche
formelle. A partir de cette sémantique, on peut écrire une formule en
logique formelle exprimant qu'un phénomène est épigénétique.
On vérifie formellement que la modélisation proposée satisfaisait cette
formule. De plus, on peut proposer des scénarii pour confronter les modèles
à l'expérimentation.
|
||||||
6 février 2003 |
Grégoire Sutre
We present a methodology and tool for verifying and certifying systems
code. The verification is based on the lazy-abstraction paradigm for
intertwining the following three logical steps: construct a predicate
abstraction from the code, model check the abstraction, and
automatically refine the abstraction based on counterexample analysis.
The certification is based on the proof-carrying code paradigm. Lazy
abstraction enables the automatic construction of small proof
certificates. The methodology is implemented in BLAST, the Berkeley
Lazy Abstraction Software verification Tool. We describe our experience
applying BLAST to Linux and Windows device drivers. Given the C code
for a driver and for a temporal-safety monitor, BLAST automatically
generates an easily checkable correctness certificate if the driver
satisfies the specification, and an error trace otherwise.
Joint work with Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula and Westley Weimer. |
||||||
30 janvier 2003 |
Frédéric Herbreteau
This work addresses the problem of computing an exact and effective
representation of the set of reachable configurations of a linear
hybrid automaton. Our solution is based on accelerating the
state-space exploration by computing symbolically the repeated effect
of cycles in the automaton transition graph. The computed sets of
configurations are represented by Real Vector Automata (RVA),
the expressive power of which goes beyond that of the first-order
additive theory of real and integer variables. This approach makes it
possible to obtain in finite time sets of configurations that cannot
be expressed as finite unions of convex regions. The main technical
contributions of the paper consist in a powerful sufficient criterion
for checking whether a hybrid transformation (i.e., with both discrete
and continuous features) can be accelerated, as well as an algorithm
for applying such an accelerated transformation on RVA. Our results
have been implemented and successfully applied to several case
studies, including the well-known leaking gas burner, and a simple
communication protocol with timers.
|
||||||
23 janvier 2003 |
Bernard Berthomieu
Les réseaux de Petri Temporels (ou de Merlin), étendent les réseaux de
Petri par des intervalles temporels associés aux transitions du
réseau. Leurs espaces d´états sont en général infinis, et à
branchement infini, même lorsque le réseau est borné. On discutera de
plusieurs abstractions finies pour les espaces d'états des réseaux
Temporels bornés. On rappellera tout d'abord la construction
classique dite "des classes d´états" [IFIP 83]. Cette construction
fournit une abstraction préservant les propriétes LTL de l'espace
d'états. On présentera ensuite une construction récente [TACAS 03]
qui préserve ses propriétés de branchement, telles qu'exprimées en
CTL* ou mu-calcul. Cette dernière abstraction produit un graphe de
classes d´états (ou états abstraits) bissimilaire à l'espace
d'états. Ces constructions, ainsi que d'autres, sont implantées dans
l'outil Tina [TINA].
|
||||||
9 janvier 2003 |
Alain Griffault
|
||||||
12 décembre 2002 |
David James Sherman
|
||||||
5 décembre 2002 |
Fabrice Kordon
Depuis plusieurs années, nous menons des travaux dans le domaine du
prototypage de systèmes répartis (modélisation, vérification,
génération automatique de programmes). Nous observons que les
solutions actuelles (principalement à base d'UML) ne sont pas
suffisantes pour capturer la dynamique du comportement de tels
systèmes. Le principal problème vient du fait que cette description
est distribuée dans différents diagrammes (comportement, séquence,
états, etc.) dont les relations ne sont pas strictement spécifiées.
Nous présentons l'état actuel de nos travaux en cours visant à intégrer les besoins des systèmes répartis dans une notation qui servirait de base à la génération automatique de squelettes de contrôle et à la vérification formelle de tels systèmes. |
||||||
21 novembre 2002 |
Anatol Slissenko
Nous décrivons une classe de logiques des prédicats avec le temps
explicite qui permettent de représenter d'une façon relativement simple
les requis et le fonctionnement des programmes temps réel. Ces logiques sont
indécidables. Cependant beaucoup de problémes réalistes se trouvent
dans une classe décidable que nous avons introduite. L'exposé présente
les logiques FOTL (first order timed logic) et une classe décidable de
problèmes de vérification. La complexité théorique et pratique sera
discutée ainsi que des questions ouvertes.
(Travail commun avec D. Beauquier, LACL, Paris 12) |
||||||
24 octobre 2002 |
Claire Pagetti
AltaRica est un langage de spécification de haut niveau développé au
LABRI.
Nous proposons une extension temps réel du langage qui permet de manipuler le temps quantitatif. Cette extension formelle est à la fois syntaxique (grammaire élargie) et sémantique (sous forme de systèmes de transitions intefacés temporisés). Les résultats d'AltaRica classique sont conservés. Une fois AltaRica temporisé défini, nous avons développé un algorithme de traduction d'un noeud AltaRica temporisé en un automate temporisé. Ce qui nous permet ensuite d'utiliser des traitements standards des automates temporisés. Nous avons notamment étudié des propriétés temporelles sur des systèmes en utilisant le model checker UPPAAL. |
||||||
17 octobre 2002 |
André Arnold
|
||||||
10 octobre 2002 |
Catalin Dima
Cet exposé sera divisé en deux parties. Dans la première partie je vais
présenter plusieurs approches pour la spécification de systèmes temporisés
à l'aide des expressions régulières. Puis je vais parler du problème
d'atteignabilité "relationelle" dans les automates temporisés et de
différentes approches pour le résoudre.
|
||||||
3 octobre 2002 |
Réunion de rentrée.
|
||||||
26 septembre 2002 |
Davy Rouillard
|