Decidability And Complexity Of Process Verication

The scope of this thesis falls in the verification of infinite-state systems. Ver-ification of infinite-state systems has two aspects: equivalence checking and modelchecking. In equivalence checking, two infinite-state systems are given, and the aimis to check if the two systems are equivalent. While in model checking, the aim is tocheck if a given infinite-state system satisfies a given formula. In application, we cancheck if two systems are equivalent through equivalence checking; we can also checkif a system satisfies a given property through model checking. The study of this areato some extent enables us to verify protocols, programs, industrial designs and otherlatent infinite-state systems.Bisimulation is often chosen as the equivalence relation in equivalence check-ing. Roughly, two states are bisimilar if every transition of a state can always bematched by the other state, and the resultant states after the matching should still bebisimilar. Presently, the most popular bisimulations are strong bisimulation (by Park)and weak bisimulation (by Milner). We study another bisimulation, branching bisim-ulation which is proposed by van Glabbeek. Branching bisimulation is often as analternative to weak bisimulation. Compared with weak bisimulation, it preserves allintermediate states in silent transitions, thus it is finer than weak bisimulation; It alsohas many merits that weak bisimulation does not have, e.g., algebraic characterizationand modal logic characterization.In this thesis, we explore the problem of deciding branching bisimilarity be-tween BPA and finite-state systems, and between normed BPP and finite-state sys-tems. BPA is a simple model of sequential computation, while BPP is a simple modelof parallel computation, and normed BPP is a subclass of BPP. For BPA, we give apolynomial-time algorithm; this algorithm improves a previous one by Kucˇera et al.For normed BPP, we prove that branching bisimilarity between it and finite-state sys- tems is polynomial-time decidable.A bond in model checking is the underlying logic for system behaviors, which isoften branching/linear time logic. Here, we study EGF logic. EGF logic is formulatedby To et al, and it is comprised of EF logic and EGF operator. EGF operator has aclose relation with regular model checking, where it is called recurrence or recurrentreachability. Also, EGF operator has a meaning of fairness, which says"somethinggood will happen infinitely".In this thesis, we study the model checking problem for EGF logic on pushdownsystems and BPP. We prove that the two problems are both PSPACE-complete, andgive some results under fix formula.