Cluster abstraction of graph transformation systems

Abstract

This dissertation explores the problem of analyzing the reachable graphs of graph transformation systems. Such systems rewrite graphs according to subgraph replacement rules; we allow negative application conditions to be specified in addition. This problem is hard because the number of reachable graphs is potentially unbounded. We use abstract interpretation to compute a finite, overapproximated representation of the reachable graphs. The main idea is the notion of a cluster: We abstract the graph locally for each of its nodes such that we obtain a bounded cluster with the node and its immediate neighborhood. Then, we eliminate duplicate clusters such that we obtain a bounded abstraction for the entire graph. We lift concrete rule application to this abstraction, eventually obtaining an overapproximation of all reachable graphs. We present ASTRA, an implementation of cluster abstraction, and the merge protocol from car platooning, our main test case. This protocol enables autonomous cars to form and merge platoons consisting of a leader car and several followers, such that the leader controls speed and lane. The abstraction does well with the merge protocol, and also manages to analyze several other standard case studies from the literature, as well as test cases automatically generated from a higher-level formalism.

Diese Dissertation untersucht, wie sich die erreichbaren Graphen eines Graphtransformationssystems analysieren lassen. Solche Systeme verändern Graphen gemäß Teilgraphersetzungsregeln; wir lassen zusätzlich negative Anwendungsbedingungen zu. Dieses Problem ist schwierig, da die Anzahl der erreichbaren Graphen potentiell unbeschränkt ist. Wir benutzen abstrakte Interpretation, um eine endliche überapproximierte Darstellung der erreichbaren Graphen zu berechnen. Die Hauptidee ist der Begriff des Clusters: Wir abstrahieren den Graphen lokal für jeden seiner Knoten und erhalten einen Cluster beschränkter Größe mit diesem Knoten und seiner direkten Umgebung. Dann eliminieren wir doppelte Cluster, so dass wir eine Abstraktion beschränkter Größe für den gesamten Graphen erhalten. Wir führen dann die Regelanwendung auf dieser Abstraktion durch, wodurch wir letztlich eine Überapproximation aller erreichbaren Graphen erhalten. Wir betrachten ASTRA, eine Implementierung der Cluster-Abstraktion, und als Hauptbeispiel das Merge-Protokoll aus dem Bereich automatisierter Kolonnenfahrten. Bei diesem Protokoll werden Kolonnen durch autonom fahrende Autos gebildet und verschmolzen, so dass das Führungsfahrzeug Geschwindigkeit und Spur kontrolliert. Die Abstraktion analysiert das gesamte Merge-Protokoll, mehrere weitere Standardfallbeispiele aus der Literatur, und auch Fallbeispiele, die aus einem Formalismus höherer Ordnung automatisch generiert wurden.