Symbolic register automata

DOI10.1007/978-3-030-25540-4_1arXiv1811.06968MaRDI QIDQ6154571FDOQ6154571

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

Publication date: 16 February 2024

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

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.

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cited In (5)

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

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)