History-register automata
From MaRDI portal
Publication:2800969
DOI10.2168/LMCS-12(1:7)2016zbMATH Open1448.68264arXiv1209.0680OpenAlexW2549752607MaRDI QIDQ2800969FDOQ2800969
Authors: Radu Grigore, Nikos Tzevelekos 
Publication date: 19 April 2016
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata powerful enough to imitate counter machines, and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike different balances between expressiveness and effectiveness.
Full work available at URL: https://arxiv.org/abs/1209.0680
Recommendations
register automatacounter automatafreshnessautomata over infinite alphabetsinfinite systems reachability
Cited In (5)
This page was built for publication: History-register automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2800969)
