Inferring Canonical Register Automata

Abstract : In this paper, we present an extension of active automata learning to register automata, an automaton model which is capable of expressing the influence of data on control flow. Register automata operate on an infinite data domain, whose values can be assigned to registers and compared for equality. Our active learning algorithm is unique in that it directly infers the effect of data values on control flow as part of the learning process. This effect is expressed by means of registers and guarded transitions in the resulting register automata models. The application of our algorithm to a small example indicates the impact of learning register automata models: Not only are the inferred models much more expressive than finite state machines, but the prototype implementation also drastically outperforms the classic L* algorithm, even when exploiting optimal data abstraction and symmetry reduction.
Type de document :
Chapitre d'ouvrage
Kuncak, Viktor and Rybalchenko, Andrey. Verification, Model Checking, and Abstract Interpretation, 7148, Springer Berlin / Heidelberg, pp.251-266, 2012, 978-3-642-27939-3
Liste complète des métadonnées

https://hal.inria.fr/hal-00664277
Contributeur : Falk Howar <>
Soumis le : lundi 30 janvier 2012 - 11:32:09
Dernière modification le : lundi 30 janvier 2012 - 11:32:09

Identifiants

  • HAL Id : hal-00664277, version 1

Collections

Citation

Falk Howar, Bernhard Steffen, Bengt Jonsson, Sofia Cassel. Inferring Canonical Register Automata. Kuncak, Viktor and Rybalchenko, Andrey. Verification, Model Checking, and Abstract Interpretation, 7148, Springer Berlin / Heidelberg, pp.251-266, 2012, 978-3-642-27939-3. 〈hal-00664277〉

Partager

Métriques

Consultations de la notice

101