Algorithmic verification with multiple and nested parameters

Abstract

We consider parameterised verification problem, where parameters are sets and relations over these sets, typically used to denote sets of identities of replicated components and connections between the components. A specification and a system are given as (multiply) parameterised labelled transition systems, parameter values are encoded using first-order logic and correctness is understood as the traces refinement. We provide an algorithm that reduces the (infinite) set of parameter values to a finite one without changing the answer to the verification task, which can be then solved with the aid of existing tools. To the best of our knowledge, the algorithm is the most general one that is both complete and applicable to systems with multiple and nested parameters. © Springer-Verlag Berlin Heidelberg 2009.