@TechReport{ it:2013-026,
author = {Sofia Cassel and Falk Howar and Bengt Jonsson and Maik
Merten and Bernhard Steffen},
title = {A Succinct Canonical Register Automaton Model},
institution = {Department of Information Technology, Uppsala University},
department = {Division of Computer Systems},
year = {2013},
number = {2013-026},
month = dec,
note = {This is an extended version of a paper published in ATVA
2011. The extended version has been accepted for
publication in JLAP.},
abstract = {We present a novel canonical automaton model, based on
register automata, that can be used to specify protocol or
program behavior. Register automata have a finite control
structure and a finite number of registers (variables), and
process sequences of terms that carry data values from an
infinite domain. We consider register automata that compare
data values 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. This canonical
form is well suited for modeling, e.g., protocols or
program behavior. Our model can be exponentially more
succinct than previous proposals, since it filters out
'accidental' relations between data values. This opens the
way to new practical applications, e.g., in automata
learning.}
}