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.

In this work, we present a transformer-based framework for predicting future pedestrian states based on clustered historical trajectory data. In previous studies, researchers propose enhancing pedestrian trajectory predictions by using manually crafted labels to categorize pedestrian behaviors and intentions. However, these approaches often only capture a limited range of pedestrian behaviors and introduce human bias into the predictions. To alleviate the dependency on manually crafted labels, we utilize a transformer encoder coupled with hierarchical density-based clustering to automatically identify diverse behavior patterns, and use these clusters in data-driven reachability analysis. By using a transformer-based approach, we seek to enhance the representation of pedestrian trajectories and uncover characteristics or features that are subsequently used to group trajectories into different 'behavior' clusters. We show that these behavior clusters can be used with data-driven reachability analysis, yielding an end-to-end data-driven approach to predicting the future motion of pedestrians. We train and evaluate our approach on a real pedestrian dataset, showcasing its effectiveness in forecasting pedestrian movements.

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.

This literature survey explores the domain of remote driving of road vehicles within autonomous vehicles, focusing on challenges and state-of-the-art solutions related to driving feedback, latency, support control, as well as remote driving platform and real applications. The advancement towards Level-5 autonomy faces challenges, including sensor reliability and diverse scenario feasibility. Currently, remote driving is identified as vital for commercialization, however, it comes with challenges like low situational awareness, latency, and a lack of comprehensive feedback mechanisms. Solutions proposed include enhancing visual feedback, developing haptic feedback, employing prediction techniques, and use control methods to support driver. This paper reviews the existing literature on remote driving in these fields, revealing research gaps and areas for future studies. Additionally, this paper reviews the industry applications of remote driving and shows the state-of-art use cases.