Branching bisimilarity of normed BPA processes is in NExpTime

DOI10.1109/LICS.2015.25MaRDI QIDQ4635801zbMATH OpenOpenAlexFDO

Authors Wojciech Czerwiński, Petr Jančar

Publication date 23 April 2018

Published in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.0645

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Branching bisimilarity on normed BPA processes was recently shown to be decidable by Yuxi Fu (ICALP 2013) but his proof has not provided any upper complexity bound. We present a simpler approach based on relative prime decompositions that leads to a nondeterministic exponential-time algorithm; this is close to the known exponential-time lower bound.

Recommendations

• Branching bisimilarity on normed BPA is EXPTIME-complete
• Two lower bounds for BPA
• Complexity of deciding bisimilarity between normed BPA and normed BPP
• Branching bisimilarity of normed BPA processes as a rational monoid
• Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)

Cited in

(11)

• A short proof of the decidability of bisimulation for normed BPA- processes
• Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof)
• A generic framework for checking semantic equivalences between pushdown automata and finite-state automata
• scientific article; zbMATH DE number 1231554 (Why is no real title available?)
• Complexity of deciding bisimilarity between normed BPA and normed BPP
• How to Parallelize sequential processes
• Branching bisimilarity on normed BPA is EXPTIME-complete
• Branching bisimilarity of normed BPA processes as a rational monoid
• Two lower bounds for BPA
• Decidability of branching bisimulation on normed commutative context-free processes
• Bisimilarity on basic parallel processes

This page was built for publication: Branching bisimilarity of normed BPA processes is in NExpTime

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