Analysis of Dynamic Communicating Systems by Hierarchical Abstraction

Abstract

We propose a new abstraction technique for verifying topology properties
of dynamic communicating systems (DCS), a special class of infinite-state
systems. DCS are characterized by unbounded creation and destruction of
objects along with an evolving communication connectivity or topology.
We employ a lightweight graph transformation system to specify DCS. 
Hierarchical Abstraction (HA) computes a bounded over-approximation of
all topologies that can occur in a DCS directly
from its transformation rules. HA works in two steps.
First, for each connected component, called cluster, of a topology,
objects sharing a common property are summarized to one abstract object.
Then isomorphic abstract connected components are summarized to
one abstract component, called abstract cluster.
This yields a conservative approximation of all graphs that may occur 
during any DCS run.
The technique is implemented.