Reachability in pushdown register automata
DOI10.1016/J.JCSS.2017.02.008zbMATH Open1370.68185OpenAlexW1855476678MaRDI QIDQ2396722FDOQ2396722
Authors: Andrzej S. Murawski, S. J. Ramsay, Nikos Tzevelekos
Publication date: 24 May 2017
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jcss.2017.02.008
Recommendations
Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Cites Work
- A Contextual Equivalence Checker for IMJ*
- A new approach to abstract syntax with variable binding
- LTL with the freeze quantifier and register automata
- Automata and Logics for Words and Trees over an Infinite Alphabet
- Two-variable logic on data words
- Finite-memory automata
- Context-free languages over infinite alphabets
- On pebble automata for data languages with decidable emptiness problem
- Algorithmic analysis of array-accessing programs
- Finite-memory automata with non-deterministic reassignment
- Reachability analysis of pushdown automata: Application to model-checking
- On notions of regularity for data languages
- Algorithmic nominal game semantics
- Algorithmic games for full ground references
- Characterizations of Pushdown Machines in Terms of Time-Bounded Computers
- Automatic verification of recursive procedures with one integer parameter.
- Runtime Verification Based on Register Automata
- Finite state machines for strings over infinite alphabets
- Intractability of decision problems for finite-memory automata
- Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
- Game Semantic Analysis of Equivalence in IMJ
- Context-bounded analysis for concurrent programs with dynamic creation of threads
Cited In (8)
- Reactive synthesis from visibly register pushdown automata
- Reachability relations of timed pushdown automata
- Active learning for deterministic bottom-up nominal tree automata
- $$\textsc {Reach}$$ on Register Automata via History Independence
- A taxonomy and reductions for common register automata formalisms
- Decidability of the reachability problem for pushdown relational automata
- AN ALTERNATIVE CONSTRUCTION IN SYMBOLIC REACHABILITY ANALYSIS OF SECOND ORDER PUSHDOWN SYSTEMS
- Title not available (Why is that?)
This page was built for publication: Reachability in pushdown register automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2396722)