Reachability in pushdown register automata

DOI10.1016/J.JCSS.2017.02.008MaRDI QIDQ2396722zbMATH OpenOpenAlexFDO

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)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1016/j.jcss.2017.02.008

zbMATH Keywords

complexityreachabilitypushdown automataregister automatainfinite alphabets

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Reachability in pushdown register automata
• Decidability of the reachability problem for pushdown relational automata
• Reachability analysis of pushdown automata: Application to model-checking
• Reachability problem for weak multi-pushdown automata
• Reachability problem for weak multi-pushdown automata

Cites work

• A contextual equivalence checker for IMJ*
• A new approach to abstract syntax with variable binding
• Algorithmic analysis of array-accessing programs
• Algorithmic games for full ground references
• Algorithmic nominal game semantics
• Automata and Logics for Words and Trees over an Infinite Alphabet
• Automatic verification of recursive procedures with one integer parameter.
• Characterizations of Pushdown Machines in Terms of Time-Bounded Computers
• Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
• Context-bounded analysis for concurrent programs with dynamic creation of threads
• Context-free languages over infinite alphabets
• Finite state machines for strings over infinite alphabets
• Finite-memory automata
• Finite-memory automata with non-deterministic reassignment
• Game semantic analysis of equivalence in IMJ
• Intractability of decision problems for finite-memory automata
• LTL with the freeze quantifier and register automata
• On notions of regularity for data languages
• On pebble automata for data languages with decidable emptiness problem
• Reachability analysis of pushdown automata: Application to model-checking
• Runtime verification based on register automata
• Two-variable logic on data words

Cited in

(14)

• scientific article; zbMATH DE number 1886071 (Why is no real title available?)
• Binary reachability of timed-register pushdown automata and branching vector addition systems
• Push-down automata with gap-order constraints
• Reactive synthesis from visibly register pushdown automata
• Reachability in register machines with polynomial updates
• Reachability relations of timed pushdown automata
• Reachability in pushdown register automata
• Active learning for deterministic bottom-up nominal tree automata
• Reachability in higher-order-counters
• Pushdown reachability with constant treewidth
• $$\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

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)