Two Lower Bounds for BPA
Qiang Yin, Mingzhang Huang, and Chaodong He
TL;DR
This paper establishes new computational lower bounds for branching bisimilarity and the regularity problem on normed BPA, proving EXPTIME-hardness and PSPACE-hardness respectively, with detailed proofs and complexity analysis.
Contribution
It provides the first complete proof of EXPTIME-hardness for branching bisimilarity on normed BPA and refines the complexity bounds for the regularity problem.
Findings
Branching bisimilarity on normed BPA is EXPTIME-hard.
The regularity problem on normed BPA is PSPACE-hard and in EXPTIME.
Previous complexity bounds are improved and clarified.
Abstract
Branching bisimilarity on normed Basic Process Algebra (BPA) was claimed to be EXPTIME-hard in previous papers without any explicit proof. Recently it is reminded by Jan\v{c}ar that the claim is not so dependable. In this paper, we develop a new complete proof for EXPTIME-hardness of branching bisimilarity on normed BPA. We also prove the associate regularity problem on normed BPA is PSPACE-hard and in EXPTIME. This improves previous P-hard and NEXPTIME result.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Petri Nets in System Modeling · Logic, programming, and type systems