Lazy abstractions for timed automata - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2013

Lazy abstractions for timed automata

Résumé

We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We propose an algorithm that is updating LU-bounds during exploration of the search tree. In order to keep them as small as possible, the bounds are refined only when they enable a transition that is impossible in the unabstracted system. So our algorithm can be seen as a kind of lazy CEGAR algorithm for timed automata. We show that on several standard benchmarks, the algorithm is capable of keeping very small LU-bounds, and in consequence reduce the search space substantially.
Fichier principal
Vignette du fichier
m.pdf (755.07 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00775924 , version 1 (14-01-2013)
hal-00775924 , version 2 (17-01-2013)

Identifiants

Citer

Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz. Lazy abstractions for timed automata. 2013. ⟨hal-00775924v1⟩
86 Consultations
393 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More