Automated multiparameterised verification by cut-offs

Abstract

We consider multiparameterised process algebraic verification, where parameters are sets and binary relations over these sets used to respectively denote the sets of the identities of replicated components and the topology of a system. There is a cut-off result that enables such a parameterised verification task to be reduced to a finite set of finite-state ones, but no practical way to perform reduction, i.e. to compute the parameter values up to the cut-offs. The first contribution of the paper is an improved formalism that enables parameterised systems and specifications to be expressed with fewer parameters than before. The second one is a search-tree-based algorithm for computing the parameter values up to the cut-offs. The algorithm detects and discards isomorphic parameter values and is equipped with a heuristic to prune a search tree. The algorithm is implemented and the relevance of the contributions is justified by practical computations. © 2010 Springer-Verlag Berlin Heidelberg.