-
GENESIS-RL: GEnerating Natural Edge-cases with Systematic Integration of Safety considerations and Reinforcement Learning
Authors:
Hsin-Jung Yang,
Joe Beck,
Md Zahid Hasan,
Ekin Beyazit,
Subhadeep Chakraborty,
Tichakorn Wongpiromsarn,
Soumik Sarkar
Abstract:
In the rapidly evolving field of autonomous systems, the safety and reliability of the system components are fundamental requirements. These components are often vulnerable to complex and unforeseen environments, making natural edge-case generation essential for enhancing system resilience. This paper presents GENESIS-RL, a novel framework that leverages system-level safety considerations and rein…
▽ More
In the rapidly evolving field of autonomous systems, the safety and reliability of the system components are fundamental requirements. These components are often vulnerable to complex and unforeseen environments, making natural edge-case generation essential for enhancing system resilience. This paper presents GENESIS-RL, a novel framework that leverages system-level safety considerations and reinforcement learning techniques to systematically generate naturalistic edge cases. By simulating challenging conditions that mimic the real-world situations, our framework aims to rigorously test entire system's safety and reliability. Although demonstrated within the autonomous driving application, our methodology is adaptable across diverse autonomous systems. Our experimental validation, conducted on high-fidelity simulator underscores the overall effectiveness of this framework.
△ Less
Submitted 27 March, 2024;
originally announced March 2024.
-
Formal Methods for Autonomous Systems
Authors:
Tichakorn Wongpiromsarn,
Mahsa Ghasemi,
Murat Cubuktepe,
Georgios Bakirtzis,
Steven Carr,
Mustafa O. Karabag,
Cyrus Neary,
Parham Gohari,
Ufuk Topcu
Abstract:
Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees.
Th…
▽ More
Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees.
This monograph provides a survey of the current state of the art on applications of formal methods in the autonomous systems domain. We consider correct-by-construction synthesis under various formulations, including closed systems, reactive, and probabilistic settings. Beyond synthesizing systems in known environments, we address the concept of uncertainty and bound the behavior of systems that employ learning using formal methods. Further, we examine the synthesis of systems with monitoring, a mitigation technique for ensuring that once a system deviates from expected behavior, it knows a way of returning to normalcy. We also show how to overcome some limitations of formal methods themselves with learning. We conclude with future directions for formal methods in reinforcement learning, uncertainty, privacy, explainability of formal methods, and regulation and certification.
△ Less
Submitted 2 November, 2023;
originally announced November 2023.
-
Evaluation Metrics for Object Detection for Autonomous Systems
Authors:
Apurva Badithela,
Tichakorn Wongpiromsarn,
Richard M. Murray
Abstract:
This paper studies the evaluation of learning-based object detection models in conjunction with model-checking of formal specifications defined on an abstract model of an autonomous system and its environment. In particular, we define two metrics -- \emph{proposition-labeled} and \emph{class-labeled} confusion matrices -- for evaluating object detection, and we incorporate these metrics to compute…
▽ More
This paper studies the evaluation of learning-based object detection models in conjunction with model-checking of formal specifications defined on an abstract model of an autonomous system and its environment. In particular, we define two metrics -- \emph{proposition-labeled} and \emph{class-labeled} confusion matrices -- for evaluating object detection, and we incorporate these metrics to compute the satisfaction probability of system-level safety requirements. While confusion matrices have been effective for comparative evaluation of classification and object detection models, our framework fills two key gaps. First, we relate the performance of object detection to formal requirements defined over downstream high-level planning tasks. In particular, we provide empirical results that show that the choice of a good object detection algorithm, with respect to formal requirements on the overall system, significantly depends on the downstream planning and control design. Secondly, unlike the traditional confusion matrix, our metrics account for variations in performance with respect to the distance between the ego and the object being detected. We demonstrate this framework on a car-pedestrian example by computing the satisfaction probabilities for safety requirements formalized in Linear Temporal Logic (LTL).
△ Less
Submitted 19 October, 2022;
originally announced October 2022.
-
Temporal Shift Reinforcement Learning
Authors:
Deepak George Thomas,
Tichakorn Wongpiromsarn,
Ali Jannesari
Abstract:
The function approximators employed by traditional image-based Deep Reinforcement Learning (DRL) algorithms usually lack a temporal learning component and instead focus on learning the spatial component. We propose a technique, Temporal Shift Reinforcement Learning (TSRL), wherein both temporal, as well as spatial components are jointly learned. Moreover, TSRL does not require additional parameter…
▽ More
The function approximators employed by traditional image-based Deep Reinforcement Learning (DRL) algorithms usually lack a temporal learning component and instead focus on learning the spatial component. We propose a technique, Temporal Shift Reinforcement Learning (TSRL), wherein both temporal, as well as spatial components are jointly learned. Moreover, TSRL does not require additional parameters to perform temporal learning. We show that TSRL outperforms the commonly used frame stacking heuristic on both of the Atari environments we test on while beating the SOTA for one of them. This investigation has implications in the robotics as well as sequential decision-making domains.
△ Less
Submitted 26 October, 2021; v1 submitted 5 September, 2021;
originally announced September 2021.
-
The Reasonable Crowd: Towards evidence-based and interpretable models of driving behavior
Authors:
Bassam Helou,
Aditya Dusi,
Anne Collin,
Noushin Mehdipour,
Zhiliang Chen,
Cristhian Lizarazo,
Calin Belta,
Tichakorn Wongpiromsarn,
Radboud Duintjer Tebbens,
Oscar Beijbom
Abstract:
Autonomous vehicles must balance a complex set of objectives. There is no consensus on how they should do so, nor on a model for specifying a desired driving behavior. We created a dataset to help address some of these questions in a limited operating domain. The data consists of 92 traffic scenarios, with multiple ways of traversing each scenario. Multiple annotators expressed their preference be…
▽ More
Autonomous vehicles must balance a complex set of objectives. There is no consensus on how they should do so, nor on a model for specifying a desired driving behavior. We created a dataset to help address some of these questions in a limited operating domain. The data consists of 92 traffic scenarios, with multiple ways of traversing each scenario. Multiple annotators expressed their preference between pairs of scenario traversals. We used the data to compare an instance of a rulebook, carefully hand-crafted independently of the dataset, with several interpretable machine learning models such as Bayesian networks, decision trees, and logistic regression trained on the dataset. To compare driving behavior, these models use scores indicating by how much different scenario traversals violate each of 14 driving rules. The rules are interpretable and designed by subject-matter experts. First, we found that these rules were enough for these models to achieve a high classification accuracy on the dataset. Second, we found that the rulebook provides high interpretability without excessively sacrificing performance. Third, the data pointed to possible improvements in the rulebook and the rules, and to potential new rules. Fourth, we explored the interpretability vs performance trade-off by also training non-interpretable models such as a random forest. Finally, we make the dataset publicly available to encourage a discussion from the wider community on behavior specification for AVs. Please find it at github.com/bassam-motional/Reasonable-Crowd.
△ Less
Submitted 28 July, 2021;
originally announced July 2021.
-
Interpretable UAV Collision Avoidance using Deep Reinforcement Learning
Authors:
Deepak-George Thomas,
Daniil Olshanskyi,
Karter Krueger,
Tichakorn Wongpiromsarn,
Ali Jannesari
Abstract:
The significant components of any successful autonomous flight system are task completion and collision avoidance. Most deep learning algorithms successfully execute these aspects under the environment and conditions they are trained. However, they fail when subjected to novel environments. This paper presents an autonomous multi-rotor flight algorithm, using Deep Reinforcement Learning augmented…
▽ More
The significant components of any successful autonomous flight system are task completion and collision avoidance. Most deep learning algorithms successfully execute these aspects under the environment and conditions they are trained. However, they fail when subjected to novel environments. This paper presents an autonomous multi-rotor flight algorithm, using Deep Reinforcement Learning augmented with Self-Attention Models, that can effectively reason when subjected to varying inputs. In addition to their reasoning ability, they are also interpretable, enabling it to be used under real-world conditions. We have tested our algorithm under different weather conditions and environments and found it robust compared to conventional Deep Reinforcement Learning algorithms.
△ Less
Submitted 4 June, 2021; v1 submitted 25 May, 2021;
originally announced May 2021.
-
Leveraging Classification Metrics for Quantitative System-Level Analysis with Temporal Logic Specifications
Authors:
Apurva Badithela,
Tichakorn Wongpiromsarn,
Richard M. Murray
Abstract:
In many autonomy applications, performance of perception algorithms is important for effective planning and control. In this paper, we introduce a framework for computing the probability of satisfaction of formal system specifications given a confusion matrix, a statistical average performance measure for multi-class classification. We define the probability of satisfaction of a linear temporal lo…
▽ More
In many autonomy applications, performance of perception algorithms is important for effective planning and control. In this paper, we introduce a framework for computing the probability of satisfaction of formal system specifications given a confusion matrix, a statistical average performance measure for multi-class classification. We define the probability of satisfaction of a linear temporal logic formula given a specific initial state of the agent and true state of the environment. Then, we present an algorithm to construct a Markov chain that represents the system behavior under the composition of the perception and control components such that the probability of the temporal logic formula computed over the Markov chain is consistent with the probability that the temporal logic formula is satisfied by our system. We illustrate this approach on a simple example of a car with pedestrian on the sidewalk environment, and compute the probability of satisfaction of safety requirements for varying parameters of the vehicle. We also illustrate how satisfaction probability changes with varied precision and recall derived from the confusion matrix. Based on our results, we identify several opportunities for future work in develo** quantitative system-level analysis that incorporates perception models.
△ Less
Submitted 15 May, 2021;
originally announced May 2021.
-
Minimum-Violation Planning for Autonomous Systems: Theoretical and Practical Considerations
Authors:
Tichakorn Wongpiromsarn,
Konstantin Slutsky,
Emilio Frazzoli,
Ufuk Topcu
Abstract:
This paper considers the problem of computing an optimal trajectory for an autonomous system that is subject to a set of potentially conflicting rules. First, we introduce the concept of prioritized safety specifications, where each rule is expressed as a temporal logic formula with its associated weight and priority. The optimality is defined based on the violation of such prioritized safety spec…
▽ More
This paper considers the problem of computing an optimal trajectory for an autonomous system that is subject to a set of potentially conflicting rules. First, we introduce the concept of prioritized safety specifications, where each rule is expressed as a temporal logic formula with its associated weight and priority. The optimality is defined based on the violation of such prioritized safety specifications. We then introduce a class of temporal logic formulas called $\textrm{si-FLTL}_{\mathsf{G_X}}$ and develop an efficient, incremental sampling-based approach to solve this minimum-violation planning problem with guarantees on asymptotic optimality. We illustrate the application of the proposed approach in autonomous vehicles, showing that $\textrm{si-FLTL}_{\mathsf{G_X}}$ formulas are sufficiently expressive to describe many traffic rules. Finally, we discuss practical considerations and present simulation results for a vehicle overtaking scenario.
△ Less
Submitted 24 September, 2020;
originally announced September 2020.
-
Liability, Ethics, and Culture-Aware Behavior Specification using Rulebooks
Authors:
Andrea Censi,
Konstantin Slutsky,
Tichakorn Wongpiromsarn,
Dmitry Yershov,
Scott Pendleton,
James Fu,
Emilio Frazzoli
Abstract:
The behavior of self-driving cars must be compatible with an enormous set of conflicting and ambiguous objectives, from law, from ethics, from the local culture, and so on. This paper describes a new way to conveniently define the desired behavior for autonomous agents, which we use on the self-driving cars developed at nuTonomy. We define a "rulebook" as a pre-ordered set of "rules", each akin to…
▽ More
The behavior of self-driving cars must be compatible with an enormous set of conflicting and ambiguous objectives, from law, from ethics, from the local culture, and so on. This paper describes a new way to conveniently define the desired behavior for autonomous agents, which we use on the self-driving cars developed at nuTonomy. We define a "rulebook" as a pre-ordered set of "rules", each akin to a violation metric on the possible outcomes ("realizations"). The rules are partially ordered by priority. The semantics of a rulebook imposes a pre-order on the set of realizations. We study the compositional properties of the rulebooks, and we derive which operations we can allow on the rulebooks to preserve previously-introduced constraints. While we demonstrate the application of these techniques in the self-driving domain, the methods are domain-independent.
△ Less
Submitted 1 March, 2019; v1 submitted 25 February, 2019;
originally announced February 2019.
-
Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems
Authors:
Tichakorn Wongpiromsarn,
Ufuk Topcu,
Andrew Lamperski
Abstract:
We consider temporal logic verification of (possibly nonlinear) dynamical systems evolving over continuous state spaces. Our approach combines automata-based verification and the use of so-called barrier certificates. Automata-based verification allows the decomposition the verification task into a finite collection of simpler constraints over the continuous state space. The satisfaction of these…
▽ More
We consider temporal logic verification of (possibly nonlinear) dynamical systems evolving over continuous state spaces. Our approach combines automata-based verification and the use of so-called barrier certificates. Automata-based verification allows the decomposition the verification task into a finite collection of simpler constraints over the continuous state space. The satisfaction of these constraints in turn can be (potentially conservatively) proved by appropriately constructed barrier certificates. As a result, our approach, together with optimization-based search for barrier certificates, allows computational verification of dynamical systems against temporal logic properties while avoiding explicit abstractions of the dynamics as commonly done in literature.
△ Less
Submitted 14 March, 2014;
originally announced March 2014.
-
Incremental Control Synthesis in Probabilistic Environments with Temporal Logic Constraints
Authors:
Alphan Ulusoy,
Tichakorn Wongpiromsarn,
Calin Belta
Abstract:
In this paper, we present a method for optimal control synthesis of a plant that interacts with a set of agents in a graph-like environment. The control specification is given as a temporal logic statement about some properties that hold at the vertices of the environment. The plant is assumed to be deterministic, while the agents are probabilistic Markov models. The goal is to control the plant s…
▽ More
In this paper, we present a method for optimal control synthesis of a plant that interacts with a set of agents in a graph-like environment. The control specification is given as a temporal logic statement about some properties that hold at the vertices of the environment. The plant is assumed to be deterministic, while the agents are probabilistic Markov models. The goal is to control the plant such that the probability of satisfying a syntactically co-safe Linear Temporal Logic formula is maximized. We propose a computationally efficient incremental approach based on the fact that temporal logic verification is computationally cheaper than synthesis. We present a case-study where we compare our approach to the classical non-incremental approach in terms of computation time and memory usage.
△ Less
Submitted 5 September, 2012; v1 submitted 1 September, 2012;
originally announced September 2012.
-
Road Pricing for Spreading Peak Travel: Modeling and Design
Authors:
Tichakorn Wongpiromsarn,
Nan Xiao,
Keyou You,
Kai Sim,
Lihua Xie,
Emilio Frazzoli,
Daniela Rus
Abstract:
A case study of the Singapore road network provides empirical evidence that road pricing can significantly affect commuter trip timing behaviors. In this paper, we propose a model of trip timing decisions that reasonably matches the observed commuters' behaviors. Our model explicitly captures the difference in individuals' sensitivity to price, travel time and early or late arrival at destination.…
▽ More
A case study of the Singapore road network provides empirical evidence that road pricing can significantly affect commuter trip timing behaviors. In this paper, we propose a model of trip timing decisions that reasonably matches the observed commuters' behaviors. Our model explicitly captures the difference in individuals' sensitivity to price, travel time and early or late arrival at destination. New pricing schemes are suggested to better spread peak travel and reduce traffic congestion. Simulation results based on the proposed model are provided in comparison with the real data for the Singapore case study.
△ Less
Submitted 16 July, 2012;
originally announced August 2012.
-
Incremental Temporal Logic Synthesis of Control Policies for Robots Interacting with Dynamic Agents
Authors:
Tichakorn Wongpiromsarn,
Alphan Ulusoy,
Calin Belta,
Emilio Frazzoli,
Daniela Rus
Abstract:
We consider the synthesis of control policies from temporal logic specifications for robots that interact with multiple dynamic environment agents. Each environment agent is modeled by a Markov chain whereas the robot is modeled by a finite transition system (in the deterministic case) or Markov decision process (in the stochastic case). Existing results in probabilistic verification are adapted t…
▽ More
We consider the synthesis of control policies from temporal logic specifications for robots that interact with multiple dynamic environment agents. Each environment agent is modeled by a Markov chain whereas the robot is modeled by a finite transition system (in the deterministic case) or Markov decision process (in the stochastic case). Existing results in probabilistic verification are adapted to solve the synthesis problem. To partially address the state explosion issue, we propose an incremental approach where only a small subset of environment agents is incorporated in the synthesis procedure initially and more agents are successively added until we hit the constraints on computational resources. Our algorithm runs in an anytime fashion where the probability that the robot satisfies its specification increases as the algorithm progresses.
△ Less
Submitted 6 March, 2012;
originally announced March 2012.
-
Control of Probabilistic Systems under Dynamic, Partially Known Environments with Temporal Logic Specifications
Authors:
Tichakorn Wongpiromsarn,
Emilio Frazzoli
Abstract:
We consider the synthesis of control policies for probabilistic systems, modeled by Markov decision processes, operating in partially known environments with temporal logic specifications. The environment is modeled by a set of Markov chains. Each Markov chain describes the behavior of the environment in each mode. The mode of the environment, however, is not known to the system. Two control objec…
▽ More
We consider the synthesis of control policies for probabilistic systems, modeled by Markov decision processes, operating in partially known environments with temporal logic specifications. The environment is modeled by a set of Markov chains. Each Markov chain describes the behavior of the environment in each mode. The mode of the environment, however, is not known to the system. Two control objectives are considered: maximizing the expected probability and maximizing the worst-case probability that the system satisfies a given specification.
△ Less
Submitted 6 March, 2012;
originally announced March 2012.
