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.

Robots that operate in human environments need the capability to adapt their behavior to new situations. Most robots so far rely on pre-programmed behavior or machine learning algorithms trained offline with selected data. Due to the large number of possible situations robots might encounter, it becomes impractical to define or learn all behaviors before deployment, causing them to inevitably fail at some point in time. As a result of this inability to adapt to new situations, the robot might fail to successfully complete its task or achieve a goal in a way that defies people's expectations or preferences. Ideally, robots need to ability to autonomously collect additional behaviors and constraints that enable them to correct their behaviors.The topic of this dissertation is robot behavior correction using feedback from non-experts, people who are not necessarily programmers or roboticists. We explore how non-experts can help robots recover when their plan or policy fails. Furthermore, working with and around humans, robots need to adapt to user preferences. For instance, users might prefer their autonomous vehicle to adopt a defensive driving style over an aggressive one, or someone might prefer their coffee mug to be placed on the coffee table left of their chair. In many everyday situations, robots will require additional rules that do not require technical knowledge. For instance, a rule that the robot should not place the coffee mug too close to the edge of the table, or that the robot might need to open the door of a cabinet first before it can place something in it. We propose an approach that leverages knowledge from non-experts to provide input to correct robot behaviors. We identify two main types of input: what the robot should do (task goals and constraints) and how the robot should achieve its task (preferences and decision-making). This dissertation explores this approach by drawing on human-robot interaction research on robot failures, crowdsourcing, and machine learning for large-scale data collection and generation, and techniques from formal methods to ensure the safety and correctness of the robot. The work described in this dissertation is a step towards better understanding how we can design robots that can automatically correct their behavior using non-expert feedback and what the challenges are of non-expert robot behavior correction.

Robotar som agerar i miljöer med människor måste ha egenskapen att anpassa sig till nya situationer. De flesta robotar har hittills utgått från förprogrammerat beteende eller beteende från maskininlärning som tränats offline. På grund av det stora antalet möjliga situationer som en robot kan befinna sig i, så är det opraktiskt att definiera eller lära sig alla beteenden före utplacering, vilket leder till att roboten oundvikligen misslyckas vid någon tidpunkt. Resultatet av robotens oförmåga att hantera nya situationer är att den kan misslyckas med sitt uppdrag eller uppfylla sitt mål på det sättet som förväntas eller föredras. I den bästa av världar har roboten egenskapen att autonomt samla ytterligare beteenden och begränsningar som möjliggör korrekt beteende. Denna avhandlings ämne är korrigering av robotbeteende genom användning av återkoppling från personer som inte är skolade inom programmering eller robotik, d.v.s. lekmän.Vi utforskar hur lekmän kan hjälpa robotar att återhämta sig när deras plan eller policy misslyckas. Vidare måste robotar som arbetar med och runt människor kunna ta hänsyn till användarnas preferenser. Till exempel så kan användare föredra defensiva körstilar framför aggressiva körstilar hos autonoma bilar, eller en användare kan föredra att deras kaffekopp placeras på soffbordet till vänster om deras stol. I många vardagssituationer kommer robotar behöva ytterligare regler som inte kräver teknisk kunskap. Till exempel, en regel som fastslår att en kaffekopp inte ska placeras för nära kanten på ett bord, eller att roboten måste öppna dörren till ett skåp innan något kan placeras i det.Vi föreslår ett tillvägagångssätt som utnyttjar kunskap från lekmän för att förse en robot med indata för korrekta beteenden. Vi identifierar två huvudsakliga typer av indata: vad en robot borde göra (uppdrag och begränsningar), och hur en robot ska uppfylla sitt uppdrag (preferenser och beslutstagande). Denna avhandling utforskar detta tillvägagångssätt genom att använda sig av forskning inom människa-robot interaktion rörande misslyckande, crowdsourcing, och maskininlärning för storskalig datainsamling och generering, samt tekniker inom formella metoder för att garantera säkerhet och korrekthet. Arbetet som beskrivs i denna avhandling är ett steg mot en bättre förståelse av hur vi kan designa robotar som kan rätta sitt beteende automatiskt genom användning av återkoppling från lekmän samt utmaningarna inom icke-expert korrigering av robotbeteende.