The Power of Hybrid Acceleration

Abstract : This paper addresses the problem of computing symbolically the set of reachable configurations of a linear hybrid automaton. A solution proposed in earlier work consists in exploring the reachable configurations using an acceleration operator for computing the iterated effect of selected control cycles. Unfortunately, this method imposes a periodicity requirement on the data transformations labeling these cycles, that is not always satisfied in practice. This happens in particular with the important subclass of timed automata, even though it is known that the paths of such automata have a periodic behavior. The goal of this paper is to broaden substantially the applicability of hybrid acceleration. This is done by introducing powerful reduction rules, aimed at translating hybrid data transformations into equivalent ones that satisfy the periodicity criterion. In particular, we show that these rules always succeed in the case of timed automata. This makes it possible to compute an exact symbolic representation of the set of reachable configurations of a linear hybrid automaton, with a guarantee of termination over the subclass of timed automata. Compared to other known solutions to this problem, our method is simpler, and applicable to a much larger class of systems.
Type de document :
Communication dans un congrès
Ball, Thomas and Jones, Robert B. Computer Aided Verification, 18th International Conference, Aug 2006, Seattle, WA, United States. Springer, 4144, pp.438-451, 2006, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00335905
Contributeur : Frédéric Herbreteau <>
Soumis le : vendredi 31 octobre 2008 - 12:13:20
Dernière modification le : jeudi 11 janvier 2018 - 06:20:16
Document(s) archivé(s) le : mardi 9 octobre 2012 - 14:43:41

Fichier

cav06-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00335905, version 1

Collections

Citation

Bernard Boigelot, Frédéric Herbreteau. The Power of Hybrid Acceleration. Ball, Thomas and Jones, Robert B. Computer Aided Verification, 18th International Conference, Aug 2006, Seattle, WA, United States. Springer, 4144, pp.438-451, 2006, Lecture Notes in Computer Science. 〈inria-00335905〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

77