Effektiver Ansatz zur Best-Effort-Synthese von LTLf in mehrstufigen Umgebungen

Wir betrachten einen Agenten, der in einer komplexen Umgebung agiert, die durch eine mehrstufige Spezifikation modelliert ist, in der jede Stufe Nondeterminismus in der Umgebungsantwort auf die Aktionen des Agenten hinzufügt. In diesem Rahmen entwickeln wir einen effektiven Ansatz zur Best-Effort-Synthese, d.h. zur Synthese von Agentenstrategien, die gegen eine maximale Menge möglicher Umgebungsantworten in jeder Stufe gewinnen. Wir tun dies in einem Setting, in dem sowohl die mehrstufige Umgebung als auch das Ziel des Agenten in der linearen zeitlichen Logik über endlichen Spuren (LTLf) spezifiziert sind. Während theoretische Lösungstechniken, die auf Automaten über unendlichen Bäumen basieren, zuvor entwickelt wurden, umschiffen wir diese hier vollständig und konzentrieren uns auf eine DFA-basierte spieltheoretische Technik, die symbolisch effektiv implementiert werden kann. Insbesondere präsentieren wir einen nachweislich korrekten Algorithmus, der auf der separaten Lösung von DFA-basierten Spielen für jede Stufe basiert und dann die erhaltenen Lösungen on-the-fly kombiniert. Dieser Algorithmus ist linear, im Gegensatz zur exponentiellen Komplexität, in der Anzahl der Stufen und kann somit mehrstufige Umgebungen, die aus mehreren Stufen bestehen, elegant handhaben.