Regularity Problems Of Process Rewrite Systems

Verifcation on infnite state systems has been an active research topic. Not onlytheproblemsofequivalencechecking,butalsotheproblemsoffnitenessandregularitychecking are of great importance. The regularity problem asks whether there existsa fnite state system which is equivalent to a given system with respect to a certainequivalence relation.It is often proftable to carry out our correlated investigations into an equivalencechecking problem together with its regularity checking problem. Regularity checkingplays an important role in model checking and programming analysis. Practically ifthere is a feasible procedure to check the equivalence of a regular process with a fntiestate system, then we can check the equivalence between a process and a fnite statesystem in case it is regular.The issue depends crucially on the equivalence relation we choose for study. Weusually use the notion of bisimilarity, which is a type of observational semantic equiv-alence relation. It is more discriminal than the notion of language equivalence, whichbrings us great computational feasibility as well as a graceful game theoretical de-scription. Decidability and complexity issues have been extensively studied for strongbisimilarity. Nevertheless, bisimulation equivalence relations like weak bisimilarity orbranching bisimilarity introduce the internal silent actions. The introduction of silentactions brings us the precision for the description as well as the complexity for thechecking of the equivalence relation.Most of the verifcation works have been carried out in the setting of processrewrite systems. It is a general model which includes most of the infnite state mod-els, likebasicprocessalgebra(BPA),basicparallelprocess(BPP),pushdownautomata(PDA), petri net (PN), and process algebra (PA).In this paper, a conclusion of the current studies in the regularity problems on process rewrite systems is given. The results are listed and some general techniquesare analyzed. Moreover, a corollary for the undecidability for the regularity of petri netwith respect to branching bisimilarity is given.The main contribution of this papar is a solution of the regularity problem fortotally normed process algebra with respect to weak and branching bisimilarity. Thenotion of totally normed is a constraint on the rules of the input system. An equivalentcondition for the infniteness of totally normed process algebra is proved in this paper.A polynomial time deciding algorithm is given. Its time complexity is O+,where is the number of transition rules and is the maximal length of rules. Processalgebra is a general context free model, thus the algorithm works for totally normedbasic process algebra and basic parallel process as well.Further, the regularity of normed basic parallel process with respect to branchingbisimilarity and the regularity of totally normed petri net with respect to weak andbranching bisimilarity are also discussed in this paper. Some useful lemmas and proofideas are discussed in our paper.Finally, the undecidability and complexity lower bounds for regularity problemsin process rewrite systems are also mentioned. Some problems and conjectures arelisted as the future work.In summary, this paper provides an innovative framework of solving the challeng-ing theoretical problem, regularity on process rewrite systems with respect to bisim-ilarity with silent actions. For the future work, a polynomial algorithm could be im-plemented practically, and more decidability and complexity results for these series ofproblems could be proved theoretically.