On the complexity of equation solving in process algebra

Abstract

The problem of designing a system which in a given environment C should satisfy a given specification S can be formulated as “find a system P such that C(P) satisfies the specification S”. In process algebra, such problems take the form of equations. We investigate the complexity of solving such equations in process algebra. We consider the problem of deciding whether there is a process P which satisfies an equation of one of the following forms: (formula presented) where C is an arbitrary context of some process algebra, A, B and Q are given processes, S is a modal specification, ∼ (≈) is (weak) bisimulation equivalence, ⊲ is refinement between modal specifications (a generalization of bisimulation equivalence), and | and ∖L is the parallel and restriction operator of CCS respectively. The main result is that all four problems are PSPACE-hard in the size of the given contexts, processes and specifications. We also give constraints under which the first and third problem can be solved in polynomial time.