On the compositional checking of validity

Abstract

This paper is concerned with deciding whether or not assertions are valid of a parallel process using methods which are directed by the way in which the process has been composed. The assertions are drawn from a modal logic with recursion, capable of expressing a great many properties of interest. The processes are described by a language inspired by Milner's CCS and Hoare's CSP, though with some modifications. The choice of constructors allows us to handle a range of synchronisation disciplines and ensures that the processes denoted are finite state. The operations are prefixing, a non-deterministic sum, product, restriction, relabelling and a looping construct. Arbitrary parallel compositions are obtained by using a combination of product, restriction and relabelling. We are interested in deciding whether or not an assertion A is valid of a process t. If it is valid, in the sense that every reachable state of t satisfies A, we write |= A:t. This paper investigates the extent to which the composition of t can guide methods for deciding |= A:t. For instance if t were a sum t_0 + t_1 we can ask what assertions A_0 and A_1 should be valid of t_0 and t_1 respectively to ensure that A is valid of t_0 + t_1. The paper formulates new compositional methods for deciding validity, and exposes some fundamental difficulties. Algorithms are provided to reduce validity problems for prefixing, sum, relabelling, restriction and looping to validity problems for their immediate components --- all these reductions depend only on the top-level structure of terms. The existence of these reductions rests on being able to 'embed' the properties of a term in the properties, or products of properties, of its immediate subterms. Because there is not such a simple embedding for the product construction of terms, as might be expected, similar reductions become much more complicated for products; although there are general results, and the reductions can be simple in special cases, the general treatment for products meets with fundamental difficulties. Whereas reductions for products always exist for this finite state language, they demonstrably no longer just depend on the top-level (product structure) of the term; in particular, a simple assertion is exhibited for which the size of the reduction must be quadratic in the number of states of the process. An attempt is thus made to explain what makes product different from the other operations with respect to compositional reasoning, and to delimit the obstacles to automated compositional checking of validity on parallel processes.