Approximated parameterized verification of infinite-state processes with global conditions

We present a simple and effective approximated backward reachability procedure for parameterized systems with existentially and universally quantified global conditions. The individual processes operate on unbounded local variables ranging over the natural numbers. In the paper we first consider a basic model where we only allow transitions with local conditions (only the local state and local variables of the process are conditioned) and global conditions. We describe how to derive the approximate transition relation and how to analyze safety properties for the basic model. Then, we introduce the additional features one by one. This includes using shared variables, broadcast and rendez-vous communication and composition of global conditions. For each new feature, we describe how to extend the approximate transition relation and the reachability algorithm in a corresponding manner. There are at least two advantages with using gap-order constraints as a language for expressing the enabling conditions of transitions. First, they allow to handle a large class of protocols where the behavior depends on the relative ordering of values among variables, rather than the actual values of these variables. The second reason is that they define a natural ordering on the set of system configurations. In fact, it can be shown that checking safety properties (expressed as regular languages) can be translated into the reachability of sets of configurations which are upward closed with respect to this ordering. To check safety properties, we perform backward reachability analysis using gaporder constraints as a symbolic representation of upward closed sets of configurations. In the analysis, we consider a transition relation which is an over-approximation of the one induced by the parameterized system. To do that, we modify the semantics of universal quantifiers by eliminating the processes which violate the given condition. The procedure operates on an over-approximation of the transition system induced by the parameterized system. We verify mutual exclusion for complex protocols such as atomic, non-atomic and distributed versions of Lamport’s bakery algorithm.