Safety and risk-awareness are important properties for robotic systems, be it for protecting them from potentially dangerous internal states, or for avoiding collisions with obstacles and environmental hazards in disaster scenarios. Ensuring safety may be the role of more than one algorithmic layer in a system, each with varying assumptions and guarantees. This thesis investigates how to provide safety and risk-awareness in a robotic system by leveraging temporal logics, motion planning algorithms, and control theory.

Traditional control theory approaches interpret the collision avoidance safety task as a `stay-away' task; obstacles are abstracted as collections of geometric shapes, and controllers are designed to avoid each shape individually. We propose interpreting the collision avoidance problem as a `stay-within' task: the obstacle-free space is abstracted into safe regions. We propose control laws based on Control Barrier functions that guarantee that the system remains within such safe regions throughout its mission. Our results demonstrate that our controller indirectly avoids obstacles while providing the system the freedom to move within the safe regions, without the necessity to plan and track a safe trajectory. Furthermore, by extending our idea with Metric Interval Temporal Logic, we are able to consider missions with explicit time bounds. 

Temporal logics are often used to define hard constraints on motion plans for robotic systems. However, some missions may require the system to violate constraints to make progress. Therefore, we propose to soften the hard constraints when necessary. Such soft constraints, here coined as spatial preferences, are used to account for relations between the system and the environment, such as distance from obstacles. The proposed minimally-violating motion planning algorithm attempts to find trajectories that satisfy the spatial preferences as much as possible, but violate them when needed. We demonstrate the use of spatial preferences on 3D exploration scenarios with Unmanned Aerial Vehicles, where we provide safer trajectories to the system while improving exploration efficiency. 

In the last part of the thesis, we address safety in scenarios where a precise model of the environment is not available. In such scenarios, the system is required to fulfil the mission while minimizing risk, considering the imprecise model. We leverage Gaussian Processes to build approximate models of the environment, and use their posterior distributions in a risk metric. This risk metric allows us to consider less likely but possible events along the missions. To this end, we propose an online risk-aware motion planning approach, and validate it on disaster scenarios, where exposure to the unmodeled hazards might damage the system. Moreover, we explore risk-awareness between the control and mapping layers, by considering smooth approximations of Euclidean Distance Fields.

Our results indicate that our algorithms provide robotic systems with i) provably-safe controllers, ii) soft safety constraints, and iii) risk-awareness in unmodeled environments. These three properties contribute to safer and risk-aware robotic systems in the real world.

Säkerhet och riskmedvetenhet är viktiga egenskaper för robotsystem, oavsett om det är för att skydda dem från potentiellt farliga interna tillstånd eller för att undvika kollisioner med hinder och miljöfaror i katastrofscenarier. Att garantera säkerhete kan vara rollen för mer än ett lager av algoritmer i ett system, var och en med olika antaganden och garantier. Denna avhandling undersöker hur man skapar säkerhet och riskmedvetenhet i ett robotsystem genom att utnyttja tidslogik, algoritmer för rörelseplanering och reglerteori.

Traditionella metoder inom reglerteori tolkar säkerhetsuppgiften för att undvika kollisioner som en `hålla-sig-utom-uppgift'; hinder abstraheras som samlingar av geometriska former, och regulatorer utformas för att undvika varje form individuellt. Vi föreslår att problemet med kollisionsundvikande tolkas som en `hålla-sig-inom-uppgift': utrymmet fritt från hinder abstraheras till säkra regioner. Vi föreslår regulatorer baserade på kontrollbarriärfunktioner som garanterar att systemet förblir inom sådana säkra regioner under hela sitt uppdrag. Våra resultat visar att vår regulator indirekt undviker hinder samtidigt som den ger systemet frihet att röra sig inom de säkra regionerna, utan att det är nödvändigt att planera och följa en viss säker bana. Genom att utöka vår idé med tidslogik med metriska intervall kan vi dessutom hantera uppdrag med explicita tidsgränser.

Tidslogik används ofta för att definiera strikta begränsningar för rörelseplaner för robotsystem. Vissa uppdrag kan dock kräva att systemet bryter mot begränsningar för att göra framsteg. Därför föreslår vi att mjuka upp de strikta begränsningarna vid behov. Sådana följsamma begränsningar, här kallade för rumsliga preferenser, används för att redogöra för relationer mellan systemet och miljön, såsom avstånd från hinder. Den föreslagna minimalt regelbrytande algoritmen för rörelseplanering försöker hitta banor som uppfyller de rumsliga preferenserna så mycket som möjligt, men kränker dem vid behov. Vi demonstrerar användningen av rumsliga preferenser i tredimensionella utforskningsscenarier med obemannade flygfordon, där vi tillhandahåller säkrare banor till systemet samtidigt som vi förbättrar utforskningseffektiviteten.

I den sista delen av avhandlingen tar vi upp säkerheten i scenarier där en exakt modell av miljön inte är tillgänglig. I sådana scenarier krävs att systemet genomför uppdraget samtidigt som risken minimeras, med hänsyn till den oprecisa modellen. Vi utnyttjar Gaussiska processer för att bygga approximativa modeller av miljön och använder deras a posteriori-fördelningar i ett riskmått. Detta riskmått gör att vi kan överväga mindre sannolika men möjliga händelser längs uppdragen. För detta ändamål föreslår vi ett direkt riskmedvetet tillvägagångssätt för planering av rörelser och validerar det i katastrofscenarier där exponering för omodellerade faror kan skada systemet. Dessutom utforskar vi riskmedvetenhet mellan reglering- och kartläggningsskikten genom att använda släta approximationer av euklidiska avståndsfält.

Våra resultat indikerar att våra algoritmer förser robotiksystem med i) bevisligen säkra regulatorer, ii) följsamma säkerhetsbegränsningar och iii) riskmedvetenhet i omodellerade miljöer. Dessa tre egenskaper bidrar till säkrare och mer riskmedvetna robotsystem i den verkliga världen.

Over the last decade, autonomous vehicles has received an increasing amount of interest from industries and research institutes. For autonomous vehicles to properly function alongside human drivers, safety guarantees are a must. Safety in traffic is more than just avoiding collisions with other drivers, it is also necessary to seamlessly act and interact in traffic.

Traffic is an environment rife with rules, both straightforward road rules, e.g. “stay in your lane”, and more subtle road rules, e.g. “give way to emergency vehicles”. Given the safety-critical nature of the environments in which an autonomous system needs to act, it is essential that the specification language chosen to encode its behaviour is able to express the full range of possible rules, both straightforward and subtle. Linear Temporal Logic (LTL) is a popular specification language used in motion planning. While LTL is suitable to express many basic rules, more elaborate rules need to incorporate continuous measures of satisfaction. For instance, it is possible to formalize ``maintain the speed limit'' in LTL. However, there is a big difference between violating the speed limit by \SI{2}{km/h} and \SI{30}{km/h}, this difference can not be quantified by LTL. Such measures are offered by Signal Temporal Logic (STL). In our work, we have used both LTL and STL to encode complex road rules including allowable distances to obstacles, as well as more complex road rules for various situations.

The aim of our work has been to formalize and verify safety guarantees for motion planning in autonomous vehicles. This thesis’ contribution encompasses three main venues of research in this area. First, current methods employed in formal synthesis for motion planning are too computationally expensive to reliably provide motion plans in real-time. To this end, we propose solutions to two different problems, scalability and guided sampling for sampling-based motion planners (Papers A and D). Second, we deal with the problem of encoding road rules for motion planning applications. We propose a new spatial-temporal quantitative semantic for STL, that allows the user to calibrate preference for efficiency (duration of mission) against perceived safety (violation of specification)(Paper B). We later show how STL can be used to encode traffic behaviours (Paper E). Third, we investigate the problem of least-violating motion planning in mixed-traffic scenarios (Papers C and E). Here we consider two different viewpoints, humans as dynamic obstacles to avoid (Paper C) and humans as participants in traffic (Paper E). We demonstrate how least-violating motion planning combined with STL, can be utilized to encode road rules in such a way as to produce different forms of driving styles that are perceivable by human users.

Självkörande fordon har under de senaste åren uppmärksammats från både industrin och akademien. För att självkörande fordon ska fungera jämte människor i trafiken är säkerhetsgarantier ett måste. Säkerhet i trafiken är mer än att bara undgå kollisioner med andra trafikanter. Det är även nödvändigt att dessa fordon kan interagera och sammarbeta med andra trafikanter. 

Trafik är en miljö med många regler, både tydliga, såsom ``stanna i ditt körfält'', och mer otydliga regler, såsom ``väj för utryckningsfordon''. Givet den säkerhetskritiska karaktären hos den miljö där det självkörande fordonet verkar, så måste ett specifikationsspråk som kan uttrycka både tydliga och subtila regler användas. Linjär tidslogik (LTL) är ett populärt specifikationsspråk som används inom banplanering. Många grundläggande regler kan beskrivas med LTL, men mer komplexa regler kräver att man kan mäta graden av tillfredsställelse. Det är möjligt att formalisera ``håll dig till hastighetsbegränsningen'' med LTL, men det är en stor skillnad mellan att bryta hastighetsbegränsningen med \SI{2}{km/h} och \SI{30}{km/h}. Denna skillnad kan inte mätas med LTL. Signal tidslogik (STL) kan användas för att mäta sådana skillnader. I vårt arbete använder vi LTL och STL för att formalisera avancerade trafikregler för att t.ex. hålla avstånd till väghinder, samt mer avancerade trafikregler i olika situationer. 

Vårt mål har varit att formalisera och verifiera säkerhetsgarantier för banplanering till självkörande fordon. Denna avhandlings bidrag innefattar tre huvudsakliga spörsmål. Till att börja med identifierar vi att nuvarande metoder för banplanering har för hög tidskomplexitet för att tillförlitligt implementeras för att uppnå banplanering i realtid. Vi föreslår lösningar för två problem inom detta område, skalbarhet, och guidad sampling för sampling-baserad banplanering (Artiklar A och D). Vidare undersöker vi problemet med att formalisera trafikregler för banplanering. Vi föreslår en ny rum-tids kvantitativ semantik för STL, som möjliggör användaren att kalibrera banans effektivitet (uppgiftens varaktighet) mot användarens uppfattade säkerhet (överträdelse av formaliserade regler)(Artikel B). Slutligen visar vi hur STL kan användas för att formalisera beteende i trafiken (Artikel E). Vi undersöker problemet med banplanering som minimerar säkerhetsöverträdelse i trafikscenarion med människor inblandade (Artiklar C och E). I dessa verk har vi två olika synvinklar, antingen människor som dynamiska hinder som måste undvikas (Artikel C), eller människor som medtrafikanter (Artikel E). Vi visar hur vår metod, kombinerad med STL, kan användas för att formalisera trafikregler på sådant sätt att det går att generera olika körstilar som kan uppfattas av människor.