Résumé de rapport du LIF

Téléchargement / Download : pdf 320k , ps.gz 296k , bibtex

Abstract

We propose a new approach for the symbolic exploration of timed automata that solves a particular aspect of the combinatory explosion occurring in the widely used clock zone automata (e.g. Kronos, UppAal). The latter approach suffers from splitting of symbolic states depending on the order of transition occurrences, even if these transitions concern unrelated components in a parallel system. Our goal is to preserve independence (commutation of transitions) from the original timed automaton to the symbolic level. We achieve this goal in three steps:

1. we lift the theory of Mazurkiewicz traces to timed words and symbolic state exploration, generalising previous work;

2. we propose a language theoretic setting for the study of the problem of symbolic state exploration, explaining difficulties of previous approaches to partial order reductions of timed automata and providing a roadmap for

3. new data structures and an algorithm for symbolic reachability in timed automata.

It has to be underlined that our algorithm solves the same problem as the classical clock zone algorithms, but in a different manner and that we preserve the worst case estimations of the classical algorithms without restricting the systems considered. We have implemented our algorithm in a new state explorer and demonstrate potential savings resulting from our approach.

Keywords

Verification, timed automata, partial order.

Résumé

Nous proposons une nouvelle approche pour les méthodes symboliques d'exploration des états accessibles pour les automates temporisés qui résoud un problème d'explosion combinatoire apparaissant avec les automates de zones qui sont largement utilisés dans les outils (c.f. Kronos, UppAal). Cette dernière approche souffre de la décomposition des états symboliques liée à l'ordre des occurrences de transition, même si celles-ci concernent des composants indépendants d'un système parallèle. Notre objectif est de préserver l'indépendance (i.e. la commutation des transitions) des automates temporisés au niveau symbolique, ce que nous obtenons en trois étapes:

1. nous adaptons la théorie des traces de Mazurkiewicz aux mots temporisés et à l'exploration des états symboliques, généralisant ainsi des travaux précédents,

2. nous proposons un cadre langage formel pour l'étude du problème de l'exploration symbolique, qui permet d'expliquer les difficultés des approches précédentes utilisant les réductions d'ordre partiel, ce qui fournit aussi un cadre pour

3. de nouvelles structures de données et un algorithme pour décider l'accessibilité symbolique pour les automates temporisés.

Il faut insister sur le fait que notre algorithme résoud le même problème que les automates de zones classiques mais avec une approche différente et que nous avons la même estimation de coût que pour les algorithmes classiques, sans faire d'hypothèse restrictive sur les systèmes utilisés. Notre algorithme de recherche d'états accessibles a été implémenté et les premières expérimentations montrent que l'approche est prometteuse.

Mots clés

Vérification, automates temporisés, ordres partiels.

Bibtex

@TECHREPORT{16-2003,
    AUTHOR	= {Denis Lugiez, Peter Niebert and S. Zennou },
    TITLE	= {{A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {16-2003},
    MONTH	= {12},
    YEAR	= {2003},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/16-2003.html},
}