Bisimulation equivalence and regularity for real-time one-counter automata
From MaRDI portal
Publication:2637644
DOI10.1016/j.jcss.2013.11.003zbMath1285.68079MaRDI QIDQ2637644
Stanislav Böhm, Petr Jančar, Stefan Göller
Publication date: 13 February 2014
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.2013.11.003
68Q45: Formal languages and automata
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Related Items
Unnamed Item, Optimally Resilient Strategies in Pushdown Safety Games, Countdown games, and simulation on (succinct) one-counter nets
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deciding bisimilarity is P-complete
- Deterministic one-counter automata
- The inclusion problem for simple languages
- A polynomial algorithm for deciding bisimilarity of normed context-free processes
- Counting on CTL\(^*\): On the expressive power of monadic path logic
- \(L(A)=L(B)\)? decidability results from complete formal systems
- \(L(A)=L(B)\)? A simplified decidability proof.
- Process rewrite systems.
- Decidability of bisimilarity for one-counter processes.
- BPA bisimilarity is EXPTIME-hard
- Semigroups, Presburger formulas, and languages
- Simulation Over One-counter Nets is PSPACE-Complete
- Decidability of DPDA Language Equivalence via First-Order Grammars
- Branching-time model checking of one-counter processes
- Reachability in Succinct and Parametric One-Counter Automata
- When Model-Checking Freeze LTL over Counter Machines Becomes Decidable
- An elementary bisimulation decision procedure for arbitrary context-free processes
- Beyond Language Equivalence on Visibly Pushdown Automata
- Model Checking FO(R) over One-Counter Processes and beyond
- Bisimilarity on Basic Process Algebra is in 2-ExpTime (an explicit proof)
- Bisimilarity of Pushdown Automata is Nonelementary
- The Bisimulation Problem for Equational Graphs of Finite Out-Degree
- Equivalence of deterministic one-counter automata is NL-complete
- Foundations of Software Science and Computation Structures
- On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic