A Succinct Canonical Register Automaton Model

Abstract : We present a novel canonical automaton model, based on register automata, that can easily be used to specify protocol or program behavior. More concretely, register automata are reminiscent of control flow graphs: they comprise a finite control structure, assignments, and conditionals, allowing to assign values of an infinite domain to registers (variables) and to compare them for equality. A major contribution is the definition of a canonical automaton representation of any language recognizable by a deterministic register automaton, by means of a Nerode congruence. Not only is this canonical form easier to comprehend than previous proposals, but it can also be exponentially more succinct than these. Key to the canonical form is the symbolic treatment of data languages, which overcomes the structural restrictions in previous formalisms, and opens the way to new practical applications.
Type de document :
Communication dans un congrès
9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, Oct 2011, Taipei, Taiwan. Springer Verlag, 6996, pp.366-380, 2011, 〈http://www.springerlink.com/content/t240177292138233/〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00647724
Contributeur : Falk Howar <>
Soumis le : vendredi 2 décembre 2011 - 15:25:41
Dernière modification le : vendredi 2 décembre 2011 - 15:49:45

Identifiants

  • HAL Id : hal-00647724, version 1

Collections

Citation

S. Cassel, F. Howar, B. Jonsson, M. Merten, B. Steffen. A Succinct Canonical Register Automaton Model. 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, Oct 2011, Taipei, Taiwan. Springer Verlag, 6996, pp.366-380, 2011, 〈http://www.springerlink.com/content/t240177292138233/〉. 〈hal-00647724〉

Partager

Métriques

Consultations de la notice

108