kirancodes.me
To Proof Maintenance & Beyond!
CAV 2019

Symbolic Register Automata

Loris D'Antoni, Tiago Ferreira, Matteo Sammartino, Alexandra Silva

PDFDOI 10.1007/978-3-030-25540-4_1dblp

Abstract

Symbolic Finite Automata and Register Automata are two orthogonal extensions of finite automata motivated by real-world problems where data may have unbounded domains. These automata address a demand for a model over large or infinite alphabets, respectively. Both automata models have interesting applications and have been successful in their own right. In this paper, we introduce Symbolic Register Automata, a new model that combines features from both symbolic and register automata, with a view on applications that were previously out of reach. We study their properties and provide algorithms for emptiness, inclusion and equivalence checking, together with experimental results.

BibTeX
@inproceedings{DAntoni-al:CAV19,
  author    = {Loris D'Antoni and
               Tiago Ferreira and
               Matteo Sammartino and
               Alexandra Silva},
  title     = {Symbolic Register Automata},
  booktitle = {CAV (Part I)},
  pages     = {3--21},
  series    = {LNCS},
  volume    = {11561},
  publisher = {Springer},
  year      = {2019},
  doi       = {10.1007/978-3-030-25540-4\_1},
}

Related papers