Spotlight Abstraction of Agents and Areas

We address the problem of automatically analysing systems that vary dynam-ically in size and topology. Typical examples of such systems include adhoc networking [1] where a routing infrastructure over a changing set of participants is created and maintained. Similar structures occur in dynamic traffic manage-ment systems like the car platooning scenario [2] where physically adjacent cars establish interlinked groups. We treat the inherent unboundedness of the state space by applying a finitary abstraction called spotlight abstraction [3,4], which is based on the data-type reduction approach [5]. The abstraction principle is heterogeneous in the sense that the behaviour of a finite number of agents is preserved while the others are only abstractly represented. Other abstraction techniques which address a similar class of systems include counter abstrac-tion [6,7], shape abstraction [8,9], partner abstraction [10,11], indexed predicate abstraction [12] and environment abstraction [13]. Let Id be a set of process identities and P a set of predicates. A system state is given by an interpretation of the predicates on the set of identities, i.e