Strict Lower Bounds for Model Checking BPA
Richard Mayr · Electronic Notes in Theoretical Computer Science · 1998
We show strict lower bounds for the complexity of several model checking problems for BPA (Basic Process Algebra). Model checking BPA with Hennessy-Milner Logic is PSPACE -hard, while model checking BPA with the (alternation-free) modal μ-calculus is EXPTIME -hard. Model checking BPA with LTL is also EXPTIME -hard. By combining these results with already established upper bounds, it follows that the model checking problems are PSPACE -complete and EXPTIME -complete, respectively.