Refine
Document Type
- Article (9)
- Monograph/Edited Volume (2)
- Postprint (1)
Language
- English (12)
Is part of the Bibliography
- yes (12)
Keywords
- Nested graph conditions (2)
- nested graph conditions (2)
- verschachtelte Graphbedingungen (2)
- Algebraic methods (1)
- Application (1)
- Attributed graph transformation (1)
- Attributed graphs (1)
- Consistency (1)
- Critical pair analysis (1)
- Critical pairs (1)
- Delta preservation (1)
- Erfüllbarkeitsanalyse (1)
- Formal modelling (1)
- Graph databases (1)
- Graph logic (1)
- Graph logics (1)
- Graph queries (1)
- Graph repair (1)
- Graph transformation (1)
- Graphreparatur (1)
- Graphtransformation (1)
- Inheritance (1)
- Initial conflicts (1)
- Institutions (1)
- Konsistenzrestauration (1)
- M-adhesive categories (1)
- M-adhesive category with NACs (1)
- M-adhesive transformation systems (1)
- Model generation (1)
- Model repair (1)
- Model-driven (1)
- Modellerzeugung (1)
- Modellreparatur (1)
- Navigational logics (1)
- Specification (1)
- Tableau method (1)
- Tableaumethode (1)
- Typed attributed graph transformation (1)
- categories (1)
- conditions (1)
- confluence (1)
- consistency restoration (1)
- critical pairs (1)
- distributed systems (1)
- embedding (1)
- engineering (1)
- grammars (1)
- graph repair (1)
- graph replacement categories (1)
- graph transformation (1)
- graph-transformations (1)
- lazy transformation (1)
- level-replacement systems (1)
- local confluence (1)
- model (1)
- model generation (1)
- model repair (1)
- nested application conditions (1)
- programs (1)
- restoration (1)
- satisfiabilitiy solving (1)
- symbolic graph transformation (1)
- synchronization (1)
- tableau method (1)
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 firstorder 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.