Model-checking and control of self-assembly

Graph grammars can be used to model highly distributed systems where local interaction rules control formation or self-assembly tasks. In this paper, we explore model-checking graph grammar systems, introducing the zero-one-many collapse as a way of reducing the usually enormous number of states and transitions produced by a graph grammar system. From this collapse, we also define a canonical initial graph, that captures some of the characteristic behavior of larger graphs with the same zero-one-many collapse. Finally, we show through examples how these results allow us to effectively reason about the behavior of a graph grammar - and also how to improve a graph grammar based on an analysis of its collapsed Kripke structures