@article {IOPORT.06021321,
    author       = {Mazur, Tomasz and Lowe, Gavin},
    title        = {A type reduction theory for systems with replicated components.},
    year         = {2012},
    journal      = {Logical Methods in Computer Science [electronic only]},
    volume       = {8},
    number       = {1},
    issn         = {1860-5974},
    pages        = {Paper No. 4, 61 p., electronic only},
    publisher    = {Logical Methods in Computer Science c/o Institute of Theoretical Computer Science, Technical University of Braunschweig, Braunschweig},
    doi          = {10.2168/LMCS-8(1:4)2012},
    abstract     = {Summary: The parameterised model checking problem (PMCP) asks whether an implementation $\mathrm{Impl}(t)$ satisfies a specification $\mathrm{Spec}(t)$ for all instantiations of parameter $t$. In general, $t$ can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this paper is automation of uniform verification of a subclass of PMCP with the 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 a given verification problem, establishes a function $\varphi $ that maps all (sufficiently large) instantiations $T$ of the parameter to some fixed type $\widehat T$ and allows us to deduce that if $\mathrm{Spec}(\widehat T)$ is refined by $\varphi (\mathrm{Impl}(T))$, then (subject to certain assumptions) $\mathrm{Spec}(T)$ is refined by $\mathrm{Impl}(T)$. The theory can be used in practice by combining it with a suitable abstraction method that produces a $t$-independent process Abstr that is refined by $\varphi (\mathrm{Impl}(T))$ for all sufficiently large $T$. Then, by testing (with a model checker) if the abstract model Abstr refines $\mathrm{Spec}(\widehat T)$, we can deduce a positive answer to the original uniform verification problem. The type reduction theory relies on symbolic representation of process behaviour. We develop a symbolic operational semantics for CSP processes that satisfy certain normality requirements, and we provide a set of translation rules that allow us to concretise symbolic transition graphs. Based on this, we prove results that allow us to infer behaviours of a process instantiated with uncollapsed types from known behaviours of the same process instantiated with a reduced type. One of the main advantages of our symbolic operational semantics and the type reduction theory is their generality, which makes them applicable in a wide range of settings.},
    identifier   = {06021321},
}