A succinct canonical register automaton model for data domains with binary relations
2012 (English)In: Automated Technology for Verification and Analysis: 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings, Springer, 2012, 57-71 p.Conference paper (Refereed)
We present a novel canonical automaton model for languages over infinite data domains, that is suitable for specifying the behavior of services, protocol components, interfaces, etc. The model is based on register automata. A major contribution is a construction of succinct canonical register automata, which is parameterized on the set of relations by which elements in the data domain can be compared. We also present a Myhill Nerode-like theorem, from which minimal canonical automata can be constructed. This canonical form is as expressive as general deterministic register automata, but much better suited for modeling in practice since we lift many of the restrictions on the way variables can be accesed and stored: this allows our automata to be significantly more succinct than previously proposed canonical forms. Key to the canonical form is a symbolic treatment of data languages, which allows us to construct minimal representations whenever the set of relations can be equipped with a so-called branching framework.
Place, publisher, year, edition, pages
Springer, 2012. 57-71 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 7561
Computer and Information Science
Research subject Computer Science
IdentifiersURN: urn:nbn:se:uu:diva-186814DOI: 10.1007/978-3-642-33386-6_6ISBN: 978-3-642-33385-9OAI: oai:DiVA.org:uu-186814DiVA: diva2:576073
10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012, 3 October 2012 through 6 October 2012, Thiruvananthapuram, India