Symbolic register automata

DOI10.1007/978-3-030-25540-4_1MaRDI QIDQ6154571FDO

Authors Loris D'Antoni, Tiago A. E. Ferreira, Matteo Sammartino, Alexandra Silva

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1811.06968

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

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.

Recommendations

• Applications of symbolic finite automata
• The power of symbolic automata and transducers
• Extended symbolic finite automata and transducers
• Theoretical aspects of symbolic automata
• Minimization of symbolic automata

Cited in

(5)

• Reactive synthesis from visibly register pushdown automata
• $$\textsc {Reach}$$ on Register Automata via History Independence
• Reasoning About Data Trees Using CHCs
• Decision procedures for sequence theories
• A taxonomy and reductions for common register automata formalisms

This page was built for publication: Symbolic register automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154571)