Branching Finiteness And Regularity Problems Of Process Rewrite Systems

Equivalence verification,that is determining when two(infinite-state)systems are in some semantic sense equal,has a long tradition in the field of(theoretical)computer science.Bisimilarity verification is an important part of equivalence verification,starting in the second half of last century.Bisimilarity verification focuses on the models that are mostly infinite-state systems.Process Rewrite Systems(PRS)introduced by Mayr is a hierarchy of infinite-state systems based on the primitive operations of sequential and parallel composition.This hierarchy includes a variety of commonly-studied classes of systems such as basic process algebra,basic parallel processes,pushdown automaton and Petri nets.Since the 1980 s,there are a large number of works for bisimilarity verification on PRS.These works have made clear that it is very difficult to perform branching bisimilarity verification on process rewrite systems,which is mainly reflected in two aspects: first,on most infinite-state systems,such as one counter nets and more complicated model,the problem of branching bisimilarity equivalence checking is undecidable;second,on the basic process algebra and basic parallel processes,the decidability of the branching bisimilarity remains open.There are three types of bisimilarity verifications on PRS: the equivalence checking,the regularity checking and the finiteness checking.The key difference among them is that the former verifies the equivalence of the same model,while the latter two focus on the equivalence checking between infinite-state and finite-state systems.For the perspective of automatic verification,the requirements of regularity and finiteness checking are stronger than equivalence checking,and have more application value in industry.The results of finiteness and regularity checking are also conducive to equivalence results.This thesis focuses on the problems of branching bisimilarity finiteness and regularity verification on the process rewrite systems.We study the decidability,algorithm and complexity of such problems.The main contributions are listed as followings:Decidability of Strong Bisimilarity and Branching Bisimilarity Regularity Checking on Pushdown Automaton.Firstly,we improve the decision algorithm of the strong bisimilarity regularity problem on the pushdown automaton,then extend this algorithm to the branch bisimilarity regularity problem on the two restricted pushdown automaton models,and show them are decidable.Undecidability of Branching Bisimilarity Finiteness and Regularity Checking on Petri Nets.We prove that the branching bisimilarity finiteness and regularity on the Petri nets model are undecidable.The former one is undecidable,which is shown by a reduction from containment problem on Petri nets to the branching bisimilarity finiteness problem on Petri nets.The latter one is also undecidable by another reduction from halting problem of the Minsky counting machine to it.Lower Bound of Branching Bisimilarity Finiteness Checking on One Counter Nets(Automaton).Using the G?del numbering for the truth table of a formula,we construct the satisfiability problem of a formula into a game of branching bisimilarity finiteness on one counter nets(automaton).Then this method also reduces a DP-complete problem to this problem in polynomial time and derives that the lower bound of this problem is DP-hard.The regularity problem on one counter nets(automaton)also enjoys this lower bound.