Bisimulation equivalence and regularity for real-time one-counter automata

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

zbMATH Keywords

regularity; language equivalence; bisimulation equivalence; one-counter automaton

Mathematics Subject Classification ID

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