Decidability of invariant validation for paramaterized systems

Abstract

The control part of many concurrent and distributed programs reduces to a set Π = {p1,...,pn} of symmetric processes containing mainly assignments and tests on Boolean variables. However, the assignments, the guards and the program invariants can be Π-quantified, so the corresponding verification conditions also involve Π-quantifications. We propose a systematic procedure allowing the elimination of such quantifications for a large class of program invariants. At the core of this procedure is a variant of the Herbrand Theorem for many-sorted first-order logic with equality. © Springer-Verlag Berlin Heidelberg 2003.