skip to main content


Search for: All records

Award ID contains: 1918531

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. Multi-player games with lexicographic cost functions can capture a variety of driving and racing scenarios and are known to have pure-strategy Nash Equilibria (NE) under certain conditions. The standard Iterated Best Response (IBR) procedure for finding such equilibria can be slow because computing the best response for each agent generally involves solving a non-convex optimization problem. In this paper, we introduce a type of game which uses a lexicographic cost function. We show that for this class of games, the best responses can be effectively computed through piece-wise linear approximations. This enables us to approximate the NE using a linearized version of IBR. We show the gap between the linear approximations returned by our linearized IBR and the true best response drops asymptotically. We implement the algorithm and show that it can find approximate NE for a handful of agents driving in realistic scenarios in under 10 seconds. 
    more » « less
  2. Multi-player games with lexicographic cost functions can capture a variety of driving and racing scenarios and under certain conditions are known to have pure-strategy Nash Equilibria. The standard Iterated Best Response (IBR) procedure for finding such equilibria can be slow because, in general, computing the best response for each agent involves solving a non-convex optimization problem. In this paper, we introduce a type of game which uses a lexicographic cost function. We show that for this class of games, the best responses can be effectively computed through piece-wise linear approximations. This in turn enables us to approximate the Nash Equilibria using a linearized version of IBR. We show that the gap between the linear approximations returned by our linearized IBR and the true best response drops asymptotically. We have implemented the algorithm and our experiments show that it can find approximate Nash Equilibria for handful of agents driving in realistic scenarios in less than 10 seconds. 
    more » « less
  3. Silva, A. and (Ed.)
    We present 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of waypoints in complex workspaces. Compared to two leading tools, DryVR and Flow*, 𝖲𝖼𝖾𝗇𝖾𝖒𝗁𝖾𝖼𝗄𝖾𝗋 shows 14Γ— average speedup in verification time, even while using those very tools as reachability subroutines. 
    more » « less
  4. null (Ed.)
    Modeling is a significant piece of the puzzle in achieving safety certificates for distributed IoT and cyberphysical systems. From smart home devices to connected and autonomous vehicles, several modeling challenges like dynamic membership of participants and complex interaction patterns, span across application domains. Modeling multiple interacting vehicles can become unwieldy and impractical as vehicles change relative positions and lanes. In this paper, we present an egocentric abstraction for succinctly modeling local interactions among an arbitrary number of agents around an ego agent. These models abstract away the detailed behavior of the other agents and ignore present but physically distant agents. We show that this approach can capture interesting scenarios considered in the responsibility sensitive safety (RSS) framework for autonomous vehicles. As an illustration of how the framework can be useful for analysis, we prove safety of several highway driving scenarios using egocentric models. The proof technique also brings to the forefront the power of a classical verification approach, namely, inductive invariant assertions. We discuss possible generalizations of the analysis to other scenarios and applications. 
    more » « less
  5. Self-driving autonomous vehicles (AVs) have recently gained popularity as a research topic. The safety of AVs is exceptionally important as failure in the design of an AV could lead to catastrophic consequences. AV systems are highly heterogeneous with many different and complex components, so it is difficult to perform end-to-end testing. One solution to this dilemma is to evaluate AVs using simulated racing competition. In this thesis, we present a simulated autonomous racing competition, Generalized RAcing Intelligence Competition (GRAIC). To compete in GRAIC, participants need to submit their controller files which are deployed on a racing ego-vehicle on different race tracks. To evaluate the submitted controller, we also developed a testing pipeline, Autonomous System Operations (AutOps). AutOps is an automated, scalable, and fair testing pipeline developed using software engineering techniques such as continuous integration, containerization, and serverless computing. In order to evaluate the submitted controller in non-trivial circumstances, we populate the race tracks with scenarios, which are pre-defined traffic situations commonly seen in the real road. We present a dynamic scenario testing strategy that generates new scenarios based on results of the ego-vehicle passing through previous scenarios. 
    more » « less
  6. As autonomous systems begin to operate amongst humans, methods for safe interaction must be investigated. We consider an example of a small autonomous vehicle in a pedestrian zone that must safely maneuver around people in a free-form fashion. We investigate two key questions: How can we effectively integrate pedestrian intent estimation into our autonomous stack? Can we develop an online monitoring framework to give rigorous assurances on the safety of such human-robot interactions? We present a pedestrian intent estimation framework that can accurately predict future pedestrian trajectories given multiple possible goal locations. We integrate this into a reachability-based online monitoring and decision making scheme that formally assesses the safety of these interactions with nearly real-time performance (approximately 0.1s). These techniques are both tested in simulation and integrated on a test vehicle with a complete in-house autonomous stack, demonstrating safe interaction in real-world experiments. 
    more » « less
  7. We address the problem of synthesizing a controller for nonlinear systems with reach-avoid requirements. Our controller consists of a reference controller and a tracking controller which drives the actual trajectory to follow the reference trajectory. We identify a type of reference trajectory such that the tracking error between the actual trajectory of the closed-loop system and the reference trajectory can be bounded. Moreover, such a bound on the tracking error is independent of the reference trajectory. Using such bounds on the tracking error, we propose a method that can find a reference trajectory by solving a satisfiability problem over linear constraints. Our overall algorithm guarantees that the resulting controller can make sure every trajectory from the initial set of the system satisfies the given reach-avoid requirement. We also implement our technique in a tool FACTEST. We show that FACTEST can find controllers for four vehicle models (3–6 dimensional state space and 2–4 dimensional input space) across eight scenarios (with up to 22 obstacles), all with running time at the sub-second range. 
    more » « less
  8. null (Ed.)
    Voice assistants such as Amazon Echo (Alexa) and Google Home use microphone arrays to estimate the angle of arrival (AoA) of the human voice. This paper focuses on adding user localization as a new capability to voice assistants. For any voice command, we desire Alexa to be able to localize the user inside the home. The core challenge is two-fold: (1) accurately estimating the AoAs of multipath echoes without the knowledge of the source signal, and (2) tracing back these AoAs to reverse triangulate the user's location.We develop VoLoc, a system that proposes an iterative align-and-cancel algorithm for improved multipath AoA estimation, followed by an error-minimization technique to estimate the geometry of a nearby wall reflection. The AoAs and geometric parameters of the nearby wall are then fused to reveal the user's location. Under modest assumptions, we report localization accuracy of 0.44 m across different rooms, clutter, and user/microphone locations. VoLoc runs in near real-time but needs to hear around 15 voice commands before becoming operational. 
    more » « less