ISoLA 2024

International Symposium On Leveraging Applications of Formal Methods, Verification and Validation • Crete, Greece

Talk

It’s Safe to Play while Driving: From a Spatial Traffic Logic Towards Traffic Games

Time: Friday, 1.11

Room: Room 2

Authors: Maike Schwammberger

Abstract: Managing complex driving situations is a non-trivial task for autonomous tra!c agents. To guarantee desirable system properties of an agent’s driving decisions, formal methods o”er a wide range of approaches. In previous work, we introduced Urban Multi-lane Spatial Logic (UMLSL) to prove the safety of local driving decisions of Autonomous Tra!c Agents (ATAs), e.g. for turning left at an intersection. We now propose to integrate UMLSL into a Tra!c Game model, allowing us to verify properties of driving strategies. We use Strategy Logic to compare di”erent driving strategies w.r.t. diverse metrics, e.g. energyconsumption or timeliness. We currently intensify our work on extensions and applications of the UMLSL universe and we also reflect on some recent and future challenges for that in this paper.

Paper: Its_Safe_to_Play_while_Driving_From_a_Spatial_Traffic_Logic_Towards_Traffic_Games-paper.pdf