On the verification problem of nonregular properties for nonregular processes

Abstract

Investigate the verification problem of infinite-state processes w.r.t. nonregular properties, i.e. nondefinable by finite-state /spl omega/-automata. We consider processes in the algebra PA (Process Algebra) which provides sequential and parallel (merge) composition, nondeterministic choice and recursion. The algebra PA integrates and strictly subsumes the algebras BPA (Basic Process Algebra, i.e. context-free processes) and BPP (Basic Parallel Processes). On the other hand, we consider properties definable in a new temporal logic called CLTL (Constrained Linear-Time Logic) which is an extension of the linear-time temporal logic LTL with two kinds of constraints on traces: constraints on the numbers of occurrences of states expressed using Presburger formulas (occurrence constraints), and constraints on the order of appearance of states expressed using finite-state automata (pattern constraints). Pattern constraints allow to capture all the /spl omega/-regular properties whereas occurrence constraints allow to define nonregular properties. Then, we present (un)decidability results concerning the verification problem for the different classes of processes mentioned above and different fragments of CLTL.