Kernkonzepte
Die Autoren stellen HyperATLS vor, eine Erweiterung der Alternating-Time Temporal Logic (ATL), die es ermöglicht, strategische Fähigkeiten von Agenten zu vergleichen und Agenten zum Teilen von Strategien zu zwingen. HyperATL*S ist eine ausdrucksstarke Spezifikationssprache, die wichtige KI-bezogene Eigenschaften erfassen kann, die mit bestehenden Logiken nicht erreichbar waren.
Zusammenfassung
Die Autoren präsentieren HyperATLS, eine Erweiterung der Alternating-Time Temporal Logic (ATL), die es ermöglicht, strategische Interaktionen zwischen Agenten in Mehrbenutzer-Systemen zu vergleichen und Agenten zum Teilen von Strategien zu zwingen.
ATL* kann zwar die strategischen Fähigkeiten von Agenten (z.B. ob eine Koalition A ein Ziel letztendlich erreichen kann) ausdrücken, aber es kann keine Vergleiche zwischen mehreren strategischen Interaktionen vornehmen und auch nicht erzwingen, dass mehrere Agenten die gleiche Strategie verfolgen.
HyperATLS erweitert ATL um zwei Möglichkeiten:
- Vergleiche der Ergebnisse mehrerer strategischer Interaktionen in Bezug auf eine Hypereigenschaft, d.h. eine Eigenschaft, die sich auf mehrere Pfade gleichzeitig bezieht.
- Erzwingen, dass einige Agenten die gleiche Strategie verfolgen.
Die Autoren zeigen, dass Modelüberprüfung für HyperATL*S auf nebenläufigen Spielstrukturen entscheidbar ist. Sie implementieren ihren Modelüberprüfungsalgorithmus in einem Tool namens HyMASMC und evaluieren es an einer Reihe von Benchmarks.
Statistiken
Die Größe des Systems (|S|) variiert von 72 bis 15552 Zuständen.
Die Größe des erreichbaren Teilsystems (|Sreach|) variiert von 9 bis 113 Zuständen.
Die Verifikationszeit für HyMASMC variiert von 0,41 Sekunden bis 347,1 Sekunden.
MCMAS-SL[1G] konnte die größeren Instanzen (n=5) nicht innerhalb von 1 Stunde verifizieren.
Zitate
"HyperATLS ist eine ausdrucksstarke Spezifikationssprache, die wichtige KI-bezogene Eigenschaften erfassen kann, die mit bestehenden Logiken nicht erreichbar waren."
"Modelüberprüfung für HyperATLS auf nebenläufigen Spielstrukturen ist entscheidbar."