Better abstractions for timed automata

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. These abstractions preserve underlying simulation relations on the state space of the automaton. For both effectiveness and efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We consider the aLU abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. We prove that aLU abstraction is the biggest abstraction with respect to LU-bounds that is sound and complete for reachability. We also provide an efficient technique to use the aLU abstraction to solve the reachability problem.
Type de document :
Communication dans un congrès
LICS - 27th Annual ACM/IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnick, Croatia. IEEE, pp.375-384, 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00708714
Contributeur : Frédéric Herbreteau <>
Soumis le : vendredi 15 juin 2012 - 15:32:28
Dernière modification le : jeudi 11 janvier 2018 - 06:20:16

Identifiants

  • HAL Id : hal-00708714, version 1
  • ARXIV : 1110.3705

Collections

Citation

Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz. Better abstractions for timed automata. LICS - 27th Annual ACM/IEEE Symposium on Logic in Computer Science - 2012, Jun 2012, Dubrovnick, Croatia. IEEE, pp.375-384, 2012. 〈hal-00708714〉

Partager

Métriques

Consultations de la notice

57