Some observations on redundancy in a context

Summary

Let x be a process which can perform an action a when it is in state s. In this article we consider the situation where x is placed in a context which blocks a whenever, x is in s. The option of doing a in state s is redundant in such a context and x can be replaced by a process x′ which is identical to x, except for the fact that x′ cannot do a when it is in s (irrespective of the context). A simple, compositional proof technique is presented, which uses information about the traces of processes to detect redundancies in a process specification. As an illustration of the technique, a modular verification of a workcell architecture is presented.

INTRODUCTION

We are interested in the verification of distributed systems by means of algebraic manipulations. In process algebra, verifications often consist of a proof that the behaviour of an implementation IMPL equals the behaviour of a specification SPEC, after abstraction from internal activity: τ_I(IMPL) = SPEC.

The simplest strategy to prove such a statement is to derive first the transition system (process graph) for the process IMPL with the expansion theorem, apply an abstraction operator to this transition system, and then simplify the resulting system to the system for SPEC using the laws of (for instance) bisimulation semantics. This ‘global’ strategy however, is often not very practical due to combinatorial state explosion: the number of states of IMPL can be of the same order as the product of the number of states of its components. Another serious problem with this strategy is that it provides almost no ‘insight’ in the structure of the system being verified.