Verifying Infinite State Processes with Sequential and Parallel Composition

Abstract

We investigate the verification problem of infinite-state process w.r.t. logic-based specifications that express properties which may be nonregular. We consider the process algebra PA which integrates and strictly subsumes the algebras BPA (basic process algebra) and BPP (basic parallel processes), by allowing both sequential and parallel compositions as well as nondeterministic choice and recursion. Many relevant properties of PA processes are nonregular, and thus can be expressed neither by classical temporal logics nor by finite state ω-automata. Properties of particular interest are those involving constraints on numbers of occurrences of events. In order to express such properties, which are nonregular in general, we use the temporal logic PCTL which combines the branching-time temporal logic CTL with Presburger arithmetics. Then we tackle the verification problem of guarded PA processes w.r.t. PCTL formulas. We mainly prove that, while this problem is undecidable for the full PCTL, it is actually decidable for the class of guarded PA processes (and thus for the class of guarded BPA's and guarded BPP's), and a large fragment of PCTL called PCTL+.