A type reduction theory for systems with replicated components

The Parameterised Model Checking Problem asks whether an implementationImpl(t) satisfies a specification Spec(t) for all instantiations of parametert. In general, t can determine numerous entities: the number of processes usedin a network, the type of data, the capacities of buffers, etc. The main themeof this paper is automation of uniform verification of a subclass of PMCP withthe parameter of the first kind, i.e. the number of processes in the network.We use CSP as our formalism. We present a type reduction theory, which, for agiven verification problem, establishes a function \phi that maps all(sufficiently large) instantiations T of the parameter to some fixed type T^and allows us to deduce that if Spec(T^) is refined by \phi(Impl(T)), then(subject to certain assumptions) Spec(T) is refined by Impl(T). The theory canbe used in practice by combining it with a suitable abstraction method thatproduces a t-independent process Abstr that is refined by {\phi}(Impl(T)) forall sufficiently large T. Then, by testing (with a model checker) if theabstract model Abstr refines Spec(T^), we can deduce a positive answer to theoriginal uniform verification problem. The type reduction theory relies onsymbolic representation of process behaviour. We develop a symbolic operationalsemantics for CSP processes that satisfy certain normality requirements, and weprovide a set of translation rules that allow us to concretise symbolictransition graphs. Based on this, we prove results that allow us to inferbehaviours of a process instantiated with uncollapsed types from knownbehaviours of the same process instantiated with a reduced type. One of themain advantages of our symbolic operational semantics and the type reductiontheory is their generality, which makes them applicable in a wide range ofsettings