Merge-and-Shrink: A Compositional Theory of Transformations of Factored Transition Systems
Silvan Sievers and Malte Helmert
Abstract: The merge-and-shrink framework has been introduced as a
general approach for defining abstractions of large state spaces
arising in domain-independent planning and related areas. The
distinguishing characteristic of the merge-and-shrink approach is
that it operates directly on the factored representation of state
spaces, repeatedly modifying this representation through
transformations such as shrinking (abstracting a factor of
the representation), merging (combining two factors),
label reduction (abstracting the way in which different
factors interact), and pruning (removing states or
transitions of a factor).
We provide a novel view of the merge-and-shrink framework as a
``toolbox'' or ``algebra'' of transformations on factored transition
systems, with the construction of abstractions as only one possible
application. For each transformation, we study desirable properties
such as conservativeness (overapproximating the original
transition system), inducedness (absence of spurious states
and transitions), and refinability (reconstruction of paths
in the original transition system from the transformed one). We
provide the first complete characterizations of the conditions under
which these desirable properties can be achieved. We also provide
the first full formal account of factored mappings, the
mechanism used within the merge-and-shrink framework to establish
the relationship between states in the original and transformed
factored transition system.
Unlike earlier attempts to develop a theory for merge-and-shrink,
our approach is fully compositional: the properties of a sequence of
transformations can be entirely understood by the properties of the
individual transformations involved. This aspect is key to the use
of merge-and-shrink as a general toolbox for transforming factored
transition systems. New transformations can easily be added to our
theory, with compositionality taking care of the seamless
integration with the existing components. Similarly, new properties
of transformations can be integrated into the theory by showing
their compositionality and studying under which conditions they are
satisfied by the building blocks of merge-and-shrink.
*This password protected talk video will only be available after it was presented at the conference.
