Inferring Canonical Register Automata - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Chapitre D'ouvrage Année : 2012

Inferring Canonical Register Automata

Résumé

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.
Fichier non déposé

Dates et versions

hal-00664277 , version 1 (30-01-2012)

Identifiants

  • HAL Id : hal-00664277 , version 1

Citer

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⟩

Collections

CONNECT
108 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More