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

DOI10.1016/J.JCSS.2013.11.003MaRDI QIDQ2637644zbMATH OpenOpenAlexFDO

Authors Stanislav Böhm, Stefan Göller, Petr Jančar

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

bisimulation equivalencelanguage equivalenceone-counter automatonregularity

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Language equivalence of deterministic real-time one-counter automata is NL-complete
• Bisimilarity of one-counter processes is PSPACE-complete
• Equivalence of deterministic one-counter automata is NL-complete
• scientific article; zbMATH DE number 1500527
• The complexity of bisimilarity-checking for one-counter processes.

Cites work

• \(L(A)=L(B)\)? A simplified decidability proof.
• \(L(A)=L(B)\)? decidability results from complete formal systems
• A polynomial algorithm for deciding bisimilarity of normed context-free processes
• An elementary bisimulation decision procedure for arbitrary context-free processes
• Beyond Language Equivalence on Visibly Pushdown Automata
• Bisimilarity of pushdown automata is nonelementary
• Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)
• BPA bisimilarity is EXPTIME-hard
• Branching-time model checking of one-counter processes
• Counting on CTL^*: On the expressive power of monadic path logic
• Decidability of bisimilarity for one-counter processes.
• Decidability of DPDA language equivalence via first-order grammars
• Deciding bisimilarity is P-complete
• Deterministic one-counter automata
• Equivalence of deterministic one-counter automata is NL-complete
• Fast equivalence-checking for normed context-free processes
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 2038732 (Why is no real title available?)
• scientific article; zbMATH DE number 2155191 (Why is no real title available?)
• scientific article; zbMATH DE number 2086665 (Why is no real title available?)
• scientific article; zbMATH DE number 2086674 (Why is no real title available?)
• Model Checking FO(R) over One-Counter Processes and beyond
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
• One-counter Markov decision processes
• Process rewrite systems.
• Reachability in Succinct and Parametric One-Counter Automata
• Semigroups, Presburger formulas, and languages
• Simulation over one-counter nets is PSPACE-complete
• The Bisimulation Problem for Equational Graphs of Finite Out-Degree
• The inclusion problem for simple languages
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• When model-checking freeze LTL over counter machines becomes decidable

Cited in

(16)

• A note on realtime one-way synchronized alternating one-counter automata
• Language equivalence of deterministic real-time one-counter automata is NL-complete
• Bisimilarity of one-counter processes is PSPACE-complete
• Game characterization of probabilistic bisimilarity, and applications to pushdown automata
• The complexity of regular abstractions of one-counter languages
• On Büchi one-counter automata
• Regular separability of one counter automata
• Optimally Resilient Strategies in Pushdown Safety Games
• Regular separability of one counter automata
• Equivalence of deterministic one-counter automata is NL-complete
• Countdown games, and simulation on (succinct) one-counter nets
• CONCUR 2005 – Concurrency Theory
• Learning realtime one-counter automata
• Equivalence of deterministic weighted real-time one-counter automata
• Weighted one-deterministic-counter automata
• History-deterministic vector addition systems

This page was built for publication: Bisimulation equivalence and regularity for real-time one-counter automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2637644)