The road transportation network is one of the leading causes of injury and death in the world. Compared to aviation or rail, road transportation is significantly more dangerous due to its continued reliance on human drivers and the frequent occurrence of unsafe, complex traffic scenarios. Over the last decade, there has been a significant push to introduce vehicle automation into road transportation to address these challenges. By replacing the human driver, vehicle automation has the potential to  revolutionize both the safety and efficiency of the road transportation network. However, in the most recent years, we have seen slower progress in this transformation. We attribute this slow down to the continued struggle for vehicle automation to handle a long tail of unexpected traffic issues, often stemming from occlusions, sensor uncertainty, or even system faults. One approach for addressing unexpected traffic issues is the integration of remote human operators who monitor, assist, and, when needed, control the vehicles. Although a key goal of vehicle automation has been to take humans out-of-the-loop, these remote human operators form a layer of resiliency that help fill in automation gaps and mitigate failures throughout a vehicle's operation. However, by integrating remote human operators, we risk introducing new human errors into the road transportation network.

In this thesis, we seek to address this challenge by designing a new control framework that explicitly and safely integrates remote human operators into the engineering and automation of connected vehicles. Our core design approach is to closely inspect the roles that remote human operators play when supervising connected vehicles and adapt traditional control principles to these roles. For this adaptation, we detail a new methodology that combines formal methods and reachability analysis to enable online verification. We show that we can verify an operator-designed specification by constructing a computational structure called temporal logic trees using either hybrid zonotope-based or Hamilton-Jacobi reachability analysis. Through their modularity, temporal logic trees ensure that when a connected vehicle's specification is changed, the verification result can be updated in real-time. Moreover, we show that when the temporal logic trees are constructed using Hamilton-Jacobi reachability analysis, we are able to efficiently synthesize specification-compliant control sets that contain the control inputs a vehicle can implement to ensure it satisfies its requirements. Using the synthesized control sets, we design a shared autonomy system that allows a remote operator to safely control a connected vehicle in cases where automation is insufficient. By leveraging this methodology, we develop a framework that allows a remote human operator to change a connected vehicle's driving specification, automate the vehicle to complete the updated specification, and even intervene on the vehicle's operation, all with guarantees that the vehicle will comply with the specification. We validate both the technological feasibility and benefits of the developed framework on a small-scale connected vehicle testbed enabled with a 5G cellular network.

Vägnätet för vägtransport är en av de främsta orsakerna till skador och dödsfall i världen. Jämfört med flyg- eller tågtrafik är vägtransport avsevärt farligare på grund av dess fortsatta beroende av mänskliga förare och den frekventa förekomsten av osäkra, komplexa trafiksituationer. Under det senaste decenniet har det skett en betydande satsning på att införa fordonsautomation inom vägtransport för att hantera dessa utmaningar. Genom att ersätta den mänskliga föraren har fordonsautomation potential att förbättra både säkerheten och effektiviteten i vägnätet. Under de senaste åren har dock denna utveckling saktat ner. Vi tillskriver denna inbromsning fordonsautomationens fortsatta svårigheter att hantera en lång svans av oväntade trafikproblem, ofta orsakade av skymd sikt, osäkerhet i sensorer eller till och med systemfel. Ett sätt att hantera oväntade trafikproblem är att integrera fjärrstyrda mänskliga operatörer som övervakar, assisterar och vid behov styr fordonen. Trots att ett centralt mål med fordonsautomation har varit att ta bort människor ur beslutsprocessen utgör dessa fjärrstyrda operatörer ett lager av motståndskraft som hjälper till att fylla automationsluckor och hantera fel under fordonets drift. Genom att integrera fjärrstyrda operatörer riskerar vi dock att införa nya mänskliga fel i vägtransportsystemet.

I denna avhandling strävar vi efter att hantera denna utmaning genom att utforma en ny styrningsram som på ett explicit och säkert sätt integrerar fjärrstyrda mänskliga operatörer i ingenjörskonsten och automatiseringen av uppkopplade fordon. Vår huvudsakliga designansats är att noggrant analysera de roller som fjärrstyrda operatörer spelar vid övervakning av uppkopplade fordon och anpassa traditionella styrningsprinciper till dessa roller. För denna anpassning presenterar vi en ny metodik som kombinerar formella metoder och räckbarhetsanalys för att möjliggöra verifiering i realtid. Vi visar att en operatörs specificering kan verifieras genom att konstruera en beräkningsstruktur kallad temporala logikträd, med hjälp av antingen hybrid zonotopbaserad eller Hamilton-Jacobi-räckbarhetsanalys. Genom sin modularitet säkerställer temporala logikträd att när ett uppkopplat fordons specifikation ändras kan verifieringsresultatet uppdateras i realtid. Vidare visar vi att när temporala logikträd konstrueras med Hamilton-Jacobi-räckbarhetsanalys kan vi effektivt syntetisera specifikationskompatibla styrningsmängder som innehåller de styrinmatningar ett fordon kan implementera för att säkerställa att det uppfyller sina krav. Med hjälp av dessa syntetiserade styrningsmängder designar vi ett delat autonomisystem som gör det möjligt för en fjärroperatör att på ett säkert sätt styra ett uppkopplat fordon i situationer där automationen är otillräcklig. Genom att utnyttja denna metodik utvecklar vi en ramverk som gör det möjligt för en fjärrstyrd operatör att ändra ett uppkopplat fordons körspecifikation, automatisera fordonet för att slutföra den uppdaterade specifikationen och vid behov ingripa i fordonets drift – allt med garantier för att fordonet kommer att följa specifikationen. Vi validerar både den tekniska genomförbarheten och fördelarna med det utvecklade ramverket på en småskalig testbädd för uppkopplade fordon, möjliggjord av ett 5G-mobilnät.

In this paper, we introduce a set representation called polynomial logical zonotopes for performing exact and computationally efficient reachability analysis on logical systems. We prove that through this polynomial-like construction, we are able to perform all of the fundamental logical operations (XOR, NOT, XNOR, AND, NAND, OR, NOR) between sets of points exactly in a reduced space, i.e., generator space with reduced complexity. Polynomial logical zonotopes are a generalization of logical zonotopes, which are able to represent up to 2γ binary vectors using only γ generators. Due to their construction, logical zonotopes are only able to support exact computations of some logical operations (XOR, NOT, XNOR), while other operations (AND, NAND, OR, NOR) result in over-approximations in the generator space. In order to perform all fundamental logical operations exactly, we formulate a generalization of logical zonotopes that is constructed by dependent generators and exponent matrices. While we are able to perform all of the logical operations exactly, this comes with a slight increase in computational complexity compared to logical zonotopes. To illustrate and showcase the computational benefits of polynomial logical zonotopes, we present the results of performing reachability analysis on two use cases: (1) safety verification of an intersection crossing protocol and (2) reachability analysis on a high-dimensional Boolean function. Moreover, to highlight the extensibility of logical zonotopes, we include an additional use case where we perform a computationally tractable exhaustive search for the key of a linear feedback shift register.

Automated vehicles have to interact to make urban traffic safe. To handle many unplanned traffic issues, such as occlusions and system failures, automated vehicles need to cooperate with each other and the connected road infrastructure. A key component in a connected road infrastructure is the road vehicle control tower, where human operators can supervise and manage fleets of automated vehicles to ensure their safe and efficient operation. By introducing such operators, the transport system is able to mitigate a variety of complex scenarios, but at the expense of potentially introducing new human errors. In this chapter, we provide an overview of road vehicle control towers and how to guarantee safe interaction between automated driving systems and human operators. Specifically, we present our work on a behavior tree-based interaction framework that allows operators to intuitively create specifications for vehicle behavior. Using the human-defined behavior specification tree, we compute temporal logic trees, which allow us to both formally verify the feasibility of the specifications and to synthesize control sets that guarantee the specifications’ completion. Finally, we overview the implementation of a shared-autonomy approach to remote driving under the interaction framework to illustrate how it can be used for guaranteeing safety in practical use-cases.

In this work, we propose an approach for ensuring the safety of vehicles passing through an intelligent intersection. There are many proposals for the design of intelligent intersections that introduce central decision-makers to intersections for enhancing the efficiency and safety of the vehicles. To guarantee the safety of such designs, we develop a safety framework for intersections based on temporal logic and reachability analysis. We start by specifying the required behavior for all the vehicles that need to pass through the intersection as linear temporal logic formula. Then, using temporal logic trees, we break down the linear temporal logic specification into a series of Hamilton-Jacobi reachability analyses in an automated fashion. By successfully constructing the temporal logic tree through reachability analysis, we verify the feasibility of the intersection specification. By taking this approach, we enable a safety framework that is able to automatically provide safety guarantees on new intersection behavior specifications. To evaluate our approach, we implement the framework on a simulated T-intersection, where we show that we can check and guarantee the safety of vehicles with potentially conflicting paths.

In this paper, we introduce a hybrid zonotope-based approach for formally verifying the behavior of autonomous systems operating under Linear Temporal Logic (LTL) specifications. In particular, we formally verify the LTL formula by constructing temporal logic trees (TLT)s via backward reachability analysis (BRA). In previous works, TLTs are predominantly constructed with either highly general and computationally intensive level set-based BRA or simplistic and computationally efficient polytope-based BRA. In this work, we instead propose the construction of TLTs using hybrid zonotope-based BRA. By using hybrid zonotopes, we show that we are able to formally verify LTL specifications in a computationally efficient manner while still being able to represent complex geometries that are often present when deploying autonomous systems, such as non-convex, disjoint sets. Moreover, we evaluate our approach on a parking example, providing preliminary indications of how hybrid zonotopes facilitate computationally efficient formal verification of LTL specifications in environments that naturally lead to non-convex, disjoint geometries.

In this paper, we present an approach for guaranteeing the completion of complex tasks with cyber-physical systems (CPS). Specifically, we leverage temporal logic trees constructed using Hamilton-Jacobi reachability analysis to (1) check for the existence of control policies that complete a specified task and (2) develop a computationally-efficient approach to synthesize the full set of control inputs the CPS can implement in real-time to ensure the task is completed. We show that, by checking the approximation directions of each state set in the temporal logic tree, we can check if the temporal logic tree suffers from the 'leaking corner issue,' where the intersection of reachable sets yields an incorrect approximation. By ensuring a temporal logic tree has no leaking corners, we know the temporal logic tree correctly verifies the existence of control policies that satisfy the specified task. After confirming the existence of control policies, we show that we can leverage the value functions obtained through Hamilton-Jacobi reachability analysis to efficiently compute the set of control inputs the CPS can implement throughout the deployment time horizon to guarantee the completion of the specified task. Finally, we use a newly released Python toolbox to evaluate the presented approach on a simulated driving task.

Signal temporal logic (STL) formulas have been widely used as a formal language to express complex robotic specifications, thanks to their rich expressiveness and explicit time semantics. Existing approaches for STL control synthesis suffer from limited scalability with respect to the task complexity and lack of robustness against the uncertainty, for example, external disturbances. In this paper, we study the online control synthesis problem for uncertain discrete-time systems subject to STL specifications. Different from existing techniques, we propose an approach based on STL, reachability analysis, and temporal logic trees. First, based on a real-time version of STL semantics, we develop the notion of tube-based temporal logic tree (tTLT) and its recursive (offline) construction algorithm. We show that the tTLT is an under-approximation of the STL formula, in the sense that a trajectory satisfying a tTLT also satisfies the corresponding STL formula. Then, an online control synthesis algorithm is designed using the constructed tTLT. It is shown that when the STL formula is robustly satisfiable and the initial state of the system belongs to the initial root node of the tTLT, it is guaranteed that the trajectory generated by the control synthesis algorithm satisfies the STL formula. We validate the effectiveness of the proposed approach by several simulation examples and further demonstrate its practical usability on a hardware experiment. These results show that our approach is able to handle complex STL formulas with long horizons and ensure the robustness against the disturbances, which is beyond the scope of the state-of-the-art STL control synthesis approaches.

This letter presents a novel approach for reachability analysis of using constrained polynomial logical zonotopes. We perform reachability analysis to compute the set of reachable states using a recently introduced set representation called polynomial logical zonotopes, enabling computationally efficient and exact reachability analysis on logical systems. Notably, polynomial logical zonotopes address the "curse of dimensionality" when analyzing the reachability of logical systems since the set representation can represent 2(h) binary vectors using h generators. After finishing the reachability analysis, the formal verification involves verifying whether the intersection of the calculated reachable set and the unsafe set is empty or not. Polynomial logical zonotopes lack closure under intersections, prompting the formulation of constrained polynomial logical zonotopes, which preserve the computational efficiency and exactness of polynomial logical zonotopes for reachability analysis while enabling exact intersections. Additionally, an extensive empirical study is presented to demonstrate and validate the advantages of constrained polynomial logical zonotopes.

In this work, we present a small-scale testbed for evaluating the real-life performance of cellular V2X (C-V2X) applications on 5G cellular networks. Despite the growing interest and rapid technology development for V2X applications, researchers still struggle to prototype V2X applications with real wireless networks, hardware, and software in the loop in a controlled environment. To help alleviate this challenge, we present a testbed designed to accelerate development and evaluation of C-V2X applications on 5G cellular networks. By including a small-scale vehicle platform into the testbed design, we significantly reduce the time and effort required to test new C-V2X applications on 5G cellular networks. With a focus around the integration of small-scale vehicle platforms, we detail the design decisions behind the full software and hardware setup of commonly needed intelligent transport system agents (e.g. sensors, servers, vehicles). Moreover, to showcase the testbed's capability to produce industrially-relevant, real world performance evaluations, we present an evaluation of a simple test case inspired from shared situational awareness. Finally, we discuss the upcoming use of the testbed for evaluating 5G cellular network-based shared situational awareness and other C-V2X applications.

In this paper, we present a data-driven approach for safely predicting the future state sets of pedestrians. Previous approaches to predicting the future state sets of pedestrians either do not provide safety guarantees or are overly conservative. Moreover, an additional challenge is the selection or identification of a model that sufficiently captures the motion of pedestrians. To address these issues, this paper introduces the idea of splitting previously collected, historical pedestrian trajectories into different behavior modes for performing data-driven reachability analysis. Through this proposed approach, we are able to use data-driven reachability analysis to capture the future state sets of pedestrians, while being less conservative and still maintaining safety guarantees. Furthermore, this approach is modular and can support different approaches for behavior splitting. To illustrate the efficacy of the approach, we implement our method with a basic behavior-splitting module and evaluate the implementation on an open-source data set of real pedestrian trajectories. In this evaluation, we find that the modal reachable sets are less conservative and more descriptive of the future state sets of the pedestrian.