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.

Driving styles play a major role in the acceptance and use of autonomous vehicles. Yet, existing motion planning techniques can often only incorporate simple driving styles that are modeled by the developers of the planner and not tailored to the passenger. We present a new approach to encode human driving styles through the use of signal temporal logic and its robustness metrics. Specifically, we use a penalty structure that can be used in many motion planning frameworks, and calibrate its parameters to model different automated driving styles. We combine this penalty structure with a set of signal temporal logic formula, based on the Responsibility-Sensitive Safety model, to generate trajectories that we expected to correlate with three different driving styles: aggressive, neutral, and defensive. An online study showed that people perceived different parameterizations of the motion planner as unique driving styles, and that most people tend to prefer a more defensive automated driving style, which correlated to their self-reported driving style.

Motion planning is one of the core problems in a wide range of robotic applications. We discuss the use of temporal logics to include complex objectives, constraints, and preferences in motion planning algorithms and focus on three topics: the first one addresses computational tractability of Linear Temporal Logic (LTL) motion planning in systems with uncertain non-holonomic dynamics, i.e. systems whose ability to move in space is constrained. We introduce feedback motion primitives and heuristics to guide motion planning and demonstrate its use on a rover in 2D and a fixed-wing drone in 3D. Second, we introduce combined motion planning and hybrid feedback control design in order to find and follow trajectories under Metric Interval Temporal Logic (MITL) specifications. Our solution creates a path to be tracked, a sequence of obstacle-free polytopes and time stamps, and a controller that tracks the path while staying in the polytopes. Third, we focus on motion planning with spatio-temporal preferences expressed in a fragment of Signal Temporal Logic (STL). We introduce a cost function for a of a path reflecting the satisfaction/violation of the preferences based on the notion of STL spatial and temporal robustness. We integrate the cost into anytime asymptotically optimal motion planning algorithm RRT ⋆ and we show the use of the algorithm in integration with an autonomous exploration planner on a UAV.

In this work, we combine a sampling based motion planner with path non-existence verification. We show that, using our approach, it is possible to: 1) provide termination criteria to sampling-based motion planners, based on the problem specific constraints; 2) generate a method for rejection sampling that can adapt to the scenario, for instance, leveraging the relative priority between constraints. Furthermore, we describe a language-guided sampling technique based on IRRT?, that utilizes the results from the path non-existence verification procedure to reduce runtime of the underlying motion planner. The approach is studied using route and motion planning for an autonomous vehicle that aims to service transportation tasks while constrained by rules of the road. We evaluate the proposed approach using a set of real-life inspired traffic scenarios. Finally, we show that the resulting runtime of a motion planner with path non-existence verification is significantly shortened when compared to the same motion planner with traditional termination criteria, such as a resource or time limit.

We present an approach for intention-aware motion planning in an autonomous driving scenario, where a vehicle aims to traverse a road segment as quickly as possible, while constrained by road rules encoded in syntactically co-safe linear temporal logic. We show that by combining the RRTx algorithm with trajectory prediction using Mixed Observable Markov Decision Processes (MOMDP), we can achieve least-violating behavior wrt. mission completion time and the road rules, while ensuring that the likelihood of collisions remains below a user specified threshold. We illustrate the validity of our approach using simulations of a variety of traffic scenarios. 

While motion planning under temporal logic specifications has been addressed in several state-of-the-art works, spatial aspects have been so far largely neglected. In this work, we enrich the semantics of robot motion specifications by including preferences on spatial relations between its trajectory and various elements in its environment. The spatial preferences are given in a fragment of Signal Temporal Logic (STL) on top of complex missions in syntactically co-safe Linear Temporal Logic (scLTL). We propose a cost function with user-specified parameters, which determines the compromise between efficiency and spatial robustness of a trajectory.  The proposed modification of the incremental sampling-based RRT$^\star$ driven by this cost function guarantees that the motion plan (if found) simultaneously satisfies the mission and asymptotically minimize the cost. The paper includes several case studies showcasing the effects of the user-adjustable parameters on the resulting trajectories.

While centralized approaches to multi-vehicle routing problems typically provide provably optimal solutions, they do not scale well. In this paper, an algorithm for decentralized multi-vehicle routing is introduced that is often associated with significantly lower computational demands, but does not sacrifice the optimality of the found solution. In particular, we consider a fleet of autonomous vehicles traversing a road network that need to service a potentially infinite set of gradually appearing travel requests specified by their pick-up and drop-off points. The proposed algorithm synthesizes optimal assignment of the travel requests to the vehicles as well as optimal routes by utilizing Fast Marching Method (FMM) that restricts the search for the optimal assignment to a local subnetwork as opposed to the global road network. Several illustrative case studies are presented to demonstrate the effectiveness and efficiency of the approach.

In this paper we consider a fleet of self-driving cars operating in a road network governed by rules of the road, such as the Vienna Convention on Road Traffic, providing rides to customers to serve their demands with desired deadlines. We focus on the associated motion planning problem that tradesoff the demands' delays and level of violation of the rules of the road to achieve social optimum among the vehicles. Due to operating in the same environment, the interaction between the cars must be taken into account, and can induce further delays. We propose an integrated route and motion planning approach that achieves scalability with respect to the number of cars by resolving potential collision situations locally within so-called bubble spaces enclosing the conflict. The algorithms leverage the road geometries, and perform joint planning only for lead vehicles in the conflict and use queue scheduling for the remaining cars. Furthermore, a framework for storing previously resolved conflict situations is proposed, which can be use for quick querying of joint motion plans. We show the mobility-on-demand setup and effectiveness of the proposed approach in simulated case studies involving up to 10 selfdriving vehicles.

To display perceivably different driving styles is an important ability for autonomous vehicles in real-life traffic scenarios. By encouraging predictable driving styles, we can promote trust and collaboration between vehicle and human drivers in traffic. However, many motion planners lack the ability to provide different driving styles using one method.As a result, many applications are overly defensive to ensure safety, and can not be tailored to the users' preferences. In this work, we build on our previous works on encoding perceivable driving styles using Signal Temporal Logic (STL) and generating motion planning trajectories using user preferences. We refine our previously proposed spatial constraints based on the Responsibility-Sensitive Safety (RSS) model. We illustrate how the motion planner can be parameterized to produce aggressive, neutral and defensive driving behaviors, respectively.  We evaluate the resulting driving styles on a set of real-life inspired driving scenarios, modeled in the Carla simulator and provide a detailed statistical analysis of the generated trajectories.