• search hit 6 of 138
Back to Result List

Symbolic model generation for graph properties

  • 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 setGraphs 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.show moreshow less
  • Graphen sind allgegenwärtig in der Informatik. Daher ist die Verfügbarkeit von Methoden zur Darstellung und Untersuchung von Grapheigenschaften in vielen Gebieten von großer Wichtigkeit. Insbesondere ist die vollautomatische Überprüfung von Grapheigenschaften auf Erfüllbarkeit von zentraler Bedeutung. Darüberhinaus ist es in vielen Anwendungsszenarien wünschenswert diejenigen Graphen geeignet aufzuzählen, die eine Grapheigenschaft erfüllen. Im Falle einer unendlich großen Anzahl von solchen Graphen ist ein kompletter und gleichzeitig kompakter Überblick über diese Graphen anzustreben. Wir zeigen, dass die Tableau-Methode für Grapheigenschaften von Lambers und Orejas den Weg für einen Algorithmus zur Generierung von symbolischen Modellen frei gemacht hat. Wir formulieren Grapheigenschaften hierbei in einer dedizierten Logik basierend auf Graphen und Graphmorphismen. Diese Logik ist äquivalent zu der First-Order Logic auf Graphen, wie sie von Courcelle eingeführt wurde. Unser parallelisierbarer Algorithmus bestimmt graduellGraphen sind allgegenwärtig in der Informatik. Daher ist die Verfügbarkeit von Methoden zur Darstellung und Untersuchung von Grapheigenschaften in vielen Gebieten von großer Wichtigkeit. Insbesondere ist die vollautomatische Überprüfung von Grapheigenschaften auf Erfüllbarkeit von zentraler Bedeutung. Darüberhinaus ist es in vielen Anwendungsszenarien wünschenswert diejenigen Graphen geeignet aufzuzählen, die eine Grapheigenschaft erfüllen. Im Falle einer unendlich großen Anzahl von solchen Graphen ist ein kompletter und gleichzeitig kompakter Überblick über diese Graphen anzustreben. Wir zeigen, dass die Tableau-Methode für Grapheigenschaften von Lambers und Orejas den Weg für einen Algorithmus zur Generierung von symbolischen Modellen frei gemacht hat. Wir formulieren Grapheigenschaften hierbei in einer dedizierten Logik basierend auf Graphen und Graphmorphismen. Diese Logik ist äquivalent zu der First-Order Logic auf Graphen, wie sie von Courcelle eingeführt wurde. Unser parallelisierbarer Algorithmus bestimmt graduell eine endliche Menge von sogenannten symbolischen Modellen. Hierbei beschreibt jedes symbolische Modell eine Menge von endlichen Graphen, die die Grapheigenschaft erfüllen. Die symbolischen Modelle decken so gemeinsam alle endlichen Modelle ab, die die Grapheigenschaft erfüllen (Vollständigkeit) und beschreiben keine endlichen Graphen, die die Grapheigenschaft verletzen (Korrektheit). Außerdem wird kein symbolisches Modell von einem anderen abgedeckt (Kompaktheit). Letztlich ist der Algorithmus in der Lage aus jedem symbolischen Modell ein minimales endliches Modell zu extrahieren und weitere endliche Modelle abzuleiten. Der Algorithmus ist in dem neuen Werkzeug AutoGraph implementiert.show moreshow less

Download full text files

  • tbhpi115.pdfeng
    (2022KB)

    SHA-1:cf4068a73d72ced9809a5e2462bb450bbbd47a64

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Sven Schneider, Leen LambersORCiDGND, Fernando OrejasORCiD
URN:urn:nbn:de:kobv:517-opus4-103171
ISBN:978-3-86956-396-1
ISSN:1613-5652 (print)
ISSN:2191-1665 (online)
Series (Serial Number):Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam (115)
Publisher:Universitätsverlag Potsdam
Place of publication:Potsdam
Document Type:Monograph/Edited Volume
Language:English
Year of first Publication:2017
Year of Completion:2017
Publishing Institution:Universität Potsdam
Publishing Institution:Universitätsverlag Potsdam
Release Date:2017/05/03
Tag:Erfüllbarkeitsanalyse; Graphtransformation; Modellerzeugung; Tableaumethode; verschachtelte Graphbedingungen
graph transformation; model generation; nested graph conditions; satisfiabilitiy solving; tableau method
Issue:115
Pagenumber:48
RVK - Regensburg Classification:ST 230
Organizational units:An-Institute / Hasso-Plattner-Institut für Digital Engineering gGmbH
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Publication Way:Universitätsverlag Potsdam
Licence (German):License LogoKeine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht
Notes extern:In Printform erschienen im Universitätsverlag Potsdam:

Symbolic model generation for graph properties / Sven Schneider, Leen Lambers, Fernando Orejas. – Potsdam: Universitätsverlag Potsdam, 2017. – 48 S. : graph. Darst.
(Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam ; 115)
1613-5652 (print)
2191-1665 (online)
ISBN 978-3-86956-396-1
--> bestellen