Hybrid Zonotope-Based Reachability Analysis For Linear Temporal Logic Specifications

KTH, Skolan för elektroteknik och datavetenskap (EECS) 2024

In this report, we introduce a formal approach aimed at providing guarantees regarding the behavior of autonomous systems operating within dynamic environments. Our methodology is presented within the context of ensuring the safety of a vehicle throughout parking and navigation missions. To formally describe the mission, we employ Linear Temporal Logic. The evaluation of specification fulfillment is facilitated through the construction of a Temporal Logic Tree via reachability analysis. To accelerate the reachability analysis, we leverage the computational efficiency of Hybrid Zonotopes, a set representation method that allows for fast computation of set operations on non-convex disjoint sets. We illustrate how the utilization of Hybrid Zonotopes enables the description of complex and abstract tasks, as well as the ability to deal with environments containing multiple moving vehicles. To demonstrate the efficacy of our approach, we present two case studies: one in a static environment, focusing on parking in one of the available parking spots, and another in a dynamic environment, where the objective is to navigate towards the parking lot exit while avoiding collisions with other vehicles. Our results, showcase the ability of our approach to combine the expressiveness of Linear Temporal Logic with the computational efficiency of Hybrid Zonotopes to provide safety guarantees for autonomous systems operating in dynamic environments.
I denna rapport introducerar vi ett formellt tillvägagångssätt med syfte att ge garantier om beteendet hos autonoma system som verkar inom dynamiska miljöer. Vår metodik presenteras inom ramen för att säkerställa fordons säkerhet under parkerings- och navigationsuppdrag. För att formellt beskriva uppdraget använder vi Linjär Temporal Logik. Utvärderingen av specifikationens uppfyllelse underlättas genom konstruktionen av ett Temporal Logik Träd med hjälp av nåbarhetsanalys. För att påskynda nåbarhetsanalysen utnyttjar vi den beräkningsmässiga effektiviteten hos Hybrid Zonotoper, en metod för representation av mängder som möjliggör snabb beräkning av mängdoperationer på icke-konvexa och disjunkta mängder. Vi illustrerar hur användningen av Hybrid Zonotoper möjliggör beskrivningen av komplexa och abstrakta uppgifter samt förmågan att hantera miljöer med flera rörliga fordon. För att påvisa effektiviteten av vår metod presenterar vi två fallstudier: en i en statisk miljö med fokus på parkering på en av de tillgängliga parkeringsplatserna och en annan i en dynamisk miljö där målet är att navigera mot parkeringsplatsens utgång och samtidigt undvika kollisioner med andra fordon. Våra resultat visar förmågan hos vår metod att kombinera Linjär Temporal Logiks uttrycksfullhet med Hybrid Zonotopers beräkningsmässiga effektivitet för att ge säkerhetsgarantier för autonoma system som verkar i dynamiska miljöer.

Reachability Analysis; Temporal Logic; Hybrid Zonotope; Formal Methods; Räckviddsanalys; Temporal Logik; Hybrid Zonotop; Formella metoder; Electrical Engineering, Electronic Engineering, Information Engineering; Elektroteknik och elektronik; Student thesis; info:eu-repo/semantics/bachelorThesis; text

Open access content. Open access content
info:eu-repo/semantics/openAccess

application/pdf
English

UPE oai:DiVA.org:kth-351571
1457631725

UPPSALA UNIV LIBR
From OAIster®, provided by the OCLC Cooperative.

edsoai.on1457631725