Lazy abstractions for timed automata

Frédéric Herbreteau 1 B. Srivathsan 2 Igor Walukiewicz 1
1 LaBRI - Laboratoire Bordelais de Recherche en Informatique
2 Software Modeling and Verification Group
RWTH - Rheinische-Westfälische Technische Hochschule
Abstract : 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.
keyword : Verification Timed automata Abstraction
Type de document :
Communication dans un congrès
Natasha Sharygina and Helmut Veith. CAV - 24th International Conference on Computer Aided Verification - 2013, Jul 2013, Saint Petersburg, Russia. Springer, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées
https://hal.inria.fr/hal-00775924
Contributeur : Frédéric Herbreteau <>
Soumis le : jeudi 17 janvier 2013 - 16:14:40
Dernière modification le : jeudi 11 janvier 2018 - 06:20:17
Document(s) archivé(s) le : samedi 1 avril 2017 - 06:47:45

Fichiers

m.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00775924, version 2
  • ARXIV : 1301.3127

Collections

LABRI | UNIV-BORDEAUX

Citation

Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz. Lazy abstractions for timed automata. Natasha Sharygina and Helmut Veith. CAV - 24th International Conference on Computer Aided Verification - 2013, Jul 2013, Saint Petersburg, Russia. Springer, 2013, Lecture Notes in Computer Science. 〈hal-00775924v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

117

Téléchargements de fichiers

623

Contact


archive-ouverte@inria.fr