Equivalence Checking For Basic Process Algebra

Basic Process Algebra is the fundamental sequential process model in the Process Rewriting System.Compared with the finite state system,it introduces infinite states;compared to the Basic Parallel Process,it is executed sequentially and has stronger control ability;compared to the Pushdown Automaton,it can be understood as a simple single-state Pushdown Automaton.Even if the definition and computational structure of the Basic Process Algebra are very simple,the model has a certain expressive power and a wide range of applications.From a grammatical point of view,the language corresponding to the grammar defined by the system is consistent with the language that is automatically accepted by the pushdown.From a computational model perspective,the system can also simulate many sequential calculations that are more complex than finite state machines.Therefore,the exploration of the algebraic structure of the model is of great significance for the study of the basic computational model.One of the core problems of automated verification is the equivalence checking problem of infinite state systems,together with model checking and automated theorem proving.Among them,the equivalence checking can be used to determine the consis-tency of the program implementation with a given design specification.The equivalence relationship is determined by different requirement according to the strictness.Park's bisimulation,Milner's famous observational equivalence relationship are such kinds of equivalence relationship.In 1987,Baeten,Bergstra and Klop proved a famous conclu-sion:strong mutual simulation is decidable in the Basic Process Algebra.The previous conclusion of undecidability of the language equivalence checking has inspired many re-searchers to continue to study in this direction.The branching bisimulation proposed by van Glabbeek constrains the behavior of internal actions to a certain extent,which makes this equivalence relation have a more intuitive and reasonable background.The tradi-tional observation equivalence does not restrict the internal actions.The finite branching property is not valid for tradition observation equivalence,which is important to the decision process.This leads to the failure of many algorithms.This paper focuses on the Basic Process Algebra and branching bisimulation,and studies the branching bisimulation checking and regularity problem of normed Basic Process Algebra.The branching bisimulation checking problem of normed Basic Process Algebra is the first equivalence checking problem proved decidable which considers the internal actions in a sequential infinite state system.Based on the careful understanding and summarization of the existing work,this paper conducts a comprehensive nature analysis and algorithm research on the branching bisimulation of normed Basic Process Algebra.The paper concluded that the equivalence checking problem is an EXPTIME-complete problem and the regularity problem are exponential time solvable and PSPACE-hard.In the research,this paper gives a general mathematical extension of the norm on processes,studies the semantic norm in detail,and defines the descending bisimulation.By strictly defining relative bisimulation and mining its basic properties,this paper obtains the special algebraic nature of the problem:the relative decomposability of the relative version.Based on the unique decomposition,using a global greedy strategy and applying decreasing bisimulation with expansion technique is used to give the correct refinement algorithm,and the decomposition generating branching bisimilarity is obtained.Thus,we get exponential time algorithms for the branching bisimulation checking problem and regularity problem of normed Basic Process Algebra.Based on the exponential factor of the decomposition base,this paper constructs the most difficult example for the algorithm.Based on the structure of the example,we construct reductions to obtain the EXPTIME-hard lower bound of equivalence checking problem and the PSPACE-hard lower bound of the regularity problem.Most of the technical difficulties in this paper are digging the relative bisimula-tion properties and application of decreasing bisimulation with expansion to ensure the correctness of the algorithm.These are also the main technical contributions of this paper.These technologies can be applied to other related problems to develop efficient algorithm.