Cluster abstraction of graph transformation systems
Peter Backes · Publications of the UdS (Saarland University) · 2015
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 verandern Graphen gemas Teilgraphersetzungsregeln; wir lassen zusatzlich negative Anwendungsbedingungen zu. Dieses Problem ist schwierig, da die Anzahl der erreichbaren Graphen potentiell unbeschrankt ist. Wir benutzen abstrakte Interpretation, um eine endliche uberapproximierte Darstellung der erreichbaren Graphen zu berechnen. Die Hauptidee ist der Begriff des Clusters: Wir abstrahieren den Graphen lokal fur jeden seiner Knoten und erhalten einen Cluster beschrankter Grose mit diesem Knoten und seiner direkten Umgebung. Dann eliminieren wir doppelte Cluster, so dass wir eine Abstraktion beschrankter Grose fur den gesamten Graphen erhalten. Wir fuhren dann die Regelanwendung auf dieser Abstraktion durch, wodurch wir letztlich eine Uberapproximation 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 Fuhrungsfahrzeug Geschwindigkeit und Spur kontrolliert. Die Abstraktion analysiert das gesamte Merge-Protokoll, mehrere weitere Standardfallbeispiele aus der Literatur, und auch Fallbeispiele, die aus einem Formalismus hoherer Ordnung automatisch generiert wurden.