> Detailanzeige
Schneider, Sven
[Verfasser:in];
Maximova, Maria
[Verfasser:in];
Giese, Holger
[Verfasser:in]
;
Hasso-Plattner-Institut für Digital Engineering,
Universitätsverlag Potsdam,
Hasso-Plattner-Institut für Digital Engineering,
Universitätsverlag Potsdam
Invariant analysis for multi-agent graph transformation systems using k-Induction
Teilen
Literatur-
verwaltung
Direktlink
Zur
Merkliste
Lösche von
Merkliste
Per Email teilen
Auf Twitter teilen
Auf Facebook teilen
Per Whatsapp teilen
- Medientyp: E-Book
- Titel: Invariant analysis for multi-agent graph transformation systems using k-Induction
- Beteiligte: Schneider, Sven [Verfasser:in]; Maximova, Maria [Verfasser:in]; Giese, Holger [Verfasser:in]
- Körperschaft: Hasso-Plattner-Institut für Digital Engineering ; Universitätsverlag Potsdam ; Hasso-Plattner-Institut für Digital Engineering ; Universitätsverlag Potsdam
-
Erschienen:
Potsdam: Universitätsverlag Potsdam, 2022
- Erschienen in: Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam ; 143
- Umfang: 1 Online-Ressource (37 Seiten, 1723 KB); Diagramme
- Sprache: Deutsch
- DOI: 10.25932/publishup-54585
- ISBN: 9783869565316
- Identifikator:
-
Schlagwörter:
Mehragentensystem
>
Transformation
- Entstehung:
- Anmerkungen:
-
Beschreibung:
The analysis of behavioral models such as Graph Transformation Systems (GTSs) is of central importance in model-driven engineering. However, GTSs often result in intractably large or even infinite state spaces and may be equipped with multiple or even infinitely many start graphs. To mitigate these problems, static analysis techniques based on finite symbolic representations of sets of states or paths thereof have been devised. We focus on the technique of k-induction for establishing invariants specified using graph conditions. To this end, k-induction generates symbolic paths backwards from a symbolic state representing a violation of a candidate invariant to gather information on how that violation could have been reached possibly obtaining contradictions to assumed invariants. However, GTSs where multiple agents regularly perform actions independently from each other cannot be analyzed using this technique as of now as the independence among backward steps may prevent the gathering of relevant knowledge altogether. In this paper, we extend k-induction to GTSs with multiple agents thereby supporting a wide range of additional GTSs. As a running example, we consider an unbounded number of shuttles driving on a large-scale track topology, which adjust their velocity to speed limits to avoid derailing. As central contribution, we develop pruning techniques based on causality and independence among backward steps and verify that k-induction remains sound under this adaptation as well as terminates in cases where it did not terminate before.
Die Analyse von Verhaltensmodellen wie Graphtransformationssystemen (GTSs) ist von zentraler Bedeutung im Model Driven Engineering. GTSs führen jedoch häufig zu unhanhabbar großen oder sogar unendlichen Zustandsräumen und können mit mehreren oder sogar unendlich vielen Startgraphen ausgestattet sein. Um diese Probleme abzumildern, wurden statische Analysetechniken entwickelt, die auf endlichen symbolischen Darstellungen von Mengen von Zuständen oder Pfaden basieren. Wir konzentrieren uns auf die Technik der k-Induktion zur Ermittlung von Invarianten, die unter Verwendung von Graphbedingungen spezifiziert sind. Zum Zweck der Analyse erzeugt die k-Induktion symbolische Rückwärtspfade von einem symbolischen Zustand, der eine Verletzung einer Kandidateninvariante darstellt, um Informationen darüber zu sammeln, wie diese Verletzung erreicht werden konnte, wodurch möglicherweise Widersprüche zu angenommenen Invarianten gefunden werden. GTSs, bei denen mehrere Agenten regelmäßig unabhängig voneinander Aktionen ausführen, können derzeit jedoch nicht mit dieser Technik analysiert werden, da die Unabhängigkeit zwischen Rückwärtsschritten das Sammeln von relevantem Wissen möglicherweise verhindert. In diesem Artikel erweitern wir die k-Induktion auf GTSs mit mehreren Agenten und unterstützen dadurch eine breite Palette zusätzlicher GTSs. Als laufendes Beispiel betrachten wir eine unbegrenzte Anzahl von Shuttles, die auf einer großen Tracktopologie fahren und die ihre Geschwindigkeit an Geschwindigkeitsbegrenzungen anpassen, um ein Entgleisen zu vermeiden. Als zentralen Beitrag entwickeln wir Beschneidungstechniken basierend auf Kausalität und Unabhängigkeit zwischen Rückwärtsschritten und verifizieren, dass die k-Induktion unter dieser Anpassung korrekt bleibt und in Fällen terminiert, in denen sie zuvor nicht terminierte. - Zugangsstatus: Freier Zugang