In diesem Thema geht es um die Verifikation von Multi-Agenten-Systemen unter Berücksichtigung von Agenten, die natürliche strategische Fähigkeiten haben. Es wird eine angepasste Temporallogik eingeführt, mithilfe der sich solche Sachverhalte spieltheoretisch modellieren und darauf aufbauende Entscheidungsprobleme definieren lassen [2]. Darin werden passende illustrative Beispiele mit dem Werkzeug UPPAAL mithilfe praktischer Abstraktionen effizient verifiziert [1].
Innerhalb des Seminars soll die verwendete Logik inklusive Vor- und Nachteilen vorgestellt und darauf eingegangen werden, wie sich praktische Beispiele verifizieren lassen.

1. Wojciech Jamroga and Yan Kim: Practical Abstraction for Model Checking of Multi-Agent Systems (CoRR abs/2202.12016, 2022, Paper)
2. Wojciech Jamroga, Vadim Malvone and Aniello Murano: Natural Strategic Ability (Artificial Intelligence 277, 2019, Paper)