Branching Bisimilarity Checking On Infinite State Systems

Equivalence checking is one of the two popular methods in automatic verification area,the other one is model checking.The focus of equivalence checking study is bisimilarity checking and it dates back to 1980s.The challenge of bisimilarity checking is to deal with infinite state systems.Most infinite state systems can be defined in a general framework,so called Process Rewrite Systems?PRS?.There have been a lot of work on bisimilarity checking on PRS since1980s.These studies have made clear that bisimilarity checking with internal actions is very difficult on PRS in two ways:on one hand weak bisimilarity is undecidable on most infinite state systems in PRS;on the other hand decidability of weak bisimilarity on the very basic infinite state systems,BPA?Basic Process Algebra?and BPP?Basic Parallel Process?,is still open.Recent studies demonstrate that branching bisimilarity,a refined equivalence of weak bisimilarity,is decidable on both normed BPA and normed BPP.Branching bisimilarity differs from weak bisimilarity in the sense that it distinguishes state-change internal actions from state-preserving ones,and it requires that only state-preserving internal actions can be ignored.From the point of view of automatic verification,branching bisimilarity is a better equivalence than weak bisimilarity.This thesis studies the decidability,algorithm and complexity of branching bisimilarity checking on Process Rewrite Systems.The main contribution is as follows.Lower Bound of Equivalence Checking on BPA and BPP.We show that branching bisimilarity checking on normed BPA is EXPTIME-hard by a reduction from an EXPTIME-complete problem,Hit-or-Run game.Our lower bound matches the best upper bound for this problem,and it also coincides with the current best lower bound for weak bisimilarity checking on normed BPA.We also show branching bisimilarity checking on normed BPP is PSPACE-hard by a reduction from QSAT?Quantified Satisfiability?problem,ant it matches the current best lower bound of weak bisimilarity checking on normed BPP.As a byproduct of our construction we show these two lower bounds also hold for any equivalence that lies between branching bisimilarity and weak bisimilarity respectively.Complexity of Branching Bisimulation Regularity Checking.We prove that the complexity of branching bisimulation regularity on normed BPA is between PSPACE and EXPTIME.To establish the upper bound,we design an EXPTIME algorithm to decide the branching bisimulation regular property of a given BPA process,based on the branching bisimilarity checking algorithm.To establish the lower bound we construct a reduction from QSAT.The PSPACE lower bound also holds for weak bisimulation regularity on normed BPA.Undecidability of Branching Bisimilarity Checking on PRS.We show that branching bisimilarity checking on normed PA?Process Algebra?is undecidable by a reduction from Post's Correspondence Problem.We also show that branching bisimilarity checking is undecidable on normed one-counter nets by adapting Mayr's construction for weak bisimilarity checking.The construction also holds for all equivalence that lies between branching bisimilarity and weak bisimilarity.Based on these two results and the expressiveness hierarchy of Process Rewrite System,we demonstrate that there is a clear decidability frontier of branching bisimilarity checking in the PRS hierarchy.Highly Undecidability of Branching Bisimilarity Checking On Pushdown Systems.We show that branching bisimilarity checking on pushdown systems is highly undecidable.More specifically,we show it's?₁¹-complete,i.e.it is a complete problem in the first level of the analytic hierarchy.We also show that it's?₁¹-complete even if internal actions are restricted to be pushing ones.This highly undecidable situation resembles of weak bisimilarity checking on pushdown systems.Technique Contribution.To conduct the research report in this thesis,we develop Semantic Forcing technique,a refined version of Defender's Forcing technique that can be applied to branching bisimulation game.