Cluster abstraction of graph transformation systems
Peter Backes
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 letzlich 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.
