@TechReport{SLO17_TR,
AUTHOR = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
TITLE = {{Symbolic Model Generation for Graph Properties}},
YEAR = {2017},
NUMBER = {115},
ADDRESS = {Potsdam, Germany},
INSTITUTION = {Hasso Plattner Institute at the University of Potsdam},
URL = {https://publishup.uni-potsdam.de/opus4-ubp/files/10317/tbhpi115.pdf},
OPTacc_url = {},
PDF = {uploads/pdf/SLO17_TR.pdf},
OPTacc_pdf = {},
ABSTRACT = {Graphs are ubiquitous in Computer Science. For this reason,
in many areas, it is very important to have the means to express and
reason about graph properties. In particular, we want to be able to check
automatically if a given graph property is satisfiable. Actually, in most
application scenarios it is desirable to be able to explore graphs satisfying
the graph property if they exist or even to get a complete and compact
overview of the graphs satisfying the graph property.
We show that the tableau-based reasoning method for graph properties
as introduced by Lambers and Orejas paves the way for a symbolic
model generation algorithm for graph properties. Graph properties are
formulated in a dedicated logic making use of graphs and graph morphisms,
which is equivalent to first-order logic on graphs as introduced
by Courcelle. Our parallelizable algorithm gradually generates a finite
set of so-called symbolic models, where each symbolic model describes a
set of finite graphs (i.e., finite models) satisfying the graph property. The
set of symbolic models jointly describes all finite models for the graph
property (complete) and does not describe any finite graph violating the
graph property (sound). Moreover, no symbolic model is already covered
by another one (compact). Finally, the algorithm is able to generate from
each symbolic model a minimal finite model immediately and allows for
an exploration of further finite models. The algorithm is implemented in
the new tool AutoGraph.}
}