@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.}
}