Showing 1–11 of 11 results for author: Sibai, H

A Grammar for the Representation of Unmanned Aerial Vehicles with 3D Topologies

Authors: Piergiuseppe Mallozzi, Hussein Sibai, Inigo Incer, Sanjit A. Seshia, Alberto Sangiovanni-Vincentelli

Abstract: We propose a context-sensitive grammar for the systematic exploration of the design space of the topology of 3D robots, particularly unmanned aerial vehicles. It defines production rules for adding components to an incomplete design topology modeled over a 3D grid. The rules are local. The grammar is simple, yet capable of modeling most existing UAVs as well as novel ones. It can be easily general… ▽ More We propose a context-sensitive grammar for the systematic exploration of the design space of the topology of 3D robots, particularly unmanned aerial vehicles. It defines production rules for adding components to an incomplete design topology modeled over a 3D grid. The rules are local. The grammar is simple, yet capable of modeling most existing UAVs as well as novel ones. It can be easily generalized to other robotic platforms. It can be thought of as a building block for any design exploration and optimization algorithm. △ Less

Submitted 27 February, 2023; originally announced February 2023.

Certifying Safety in Reinforcement Learning under Adversarial Perturbation Attacks

Authors: Junlin Wu, Hussein Sibai, Yevgeniy Vorobeychik

Abstract: Function approximation has enabled remarkable advances in applying reinforcement learning (RL) techniques in environments with high-dimensional inputs, such as images, in an end-to-end fashion, map** such inputs directly to low-level control. Nevertheless, these have proved vulnerable to small adversarial input perturbations. A number of approaches for improving or certifying robustness of end-t… ▽ More Function approximation has enabled remarkable advances in applying reinforcement learning (RL) techniques in environments with high-dimensional inputs, such as images, in an end-to-end fashion, map** such inputs directly to low-level control. Nevertheless, these have proved vulnerable to small adversarial input perturbations. A number of approaches for improving or certifying robustness of end-to-end RL to adversarial perturbations have emerged as a result, focusing on cumulative reward. However, what is often at stake in adversarial scenarios is the violation of fundamental properties, such as safety, rather than the overall reward that combines safety with efficiency. Moreover, properties such as safety can only be defined with respect to true state, rather than the high-dimensional raw inputs to end-to-end policies. To disentangle nominal efficiency and adversarial safety, we situate RL in deterministic partially-observable Markov decision processes (POMDPs) with the goal of maximizing cumulative reward subject to safety constraints. We then propose a partially-supervised reinforcement learning (PSRL) framework that takes advantage of an additional assumption that the true state of the POMDP is known at training time. We present the first approach for certifying safety of PSRL policies under adversarial input perturbations, and two adversarial training approaches that make direct use of PSRL. Our experiments demonstrate both the efficacy of the proposed approach for certifying safety in adversarial environments, and the value of the PSRL framework coupled with adversarial training in improving certified safety while preserving high nominal reward and high-quality predictions of true state. △ Less

Submitted 28 December, 2022; originally announced December 2022.

SceneChecker: Boosting Scenario Verification using Symmetry Abstractions

Authors: Hussein Sibai, Yangge Li, Sayan Mitra

Abstract: We presentSceneChecker, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker 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. SceneChecker uses symmetry abstractions, a novel refinement algor… ▽ More We presentSceneChecker, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. SceneChecker 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. SceneChecker 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 SceneChecker 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 way-points in complex workspaces. Compared to two leading tools, DryVR and Flow*, SceneChecker shows 20x speedup in verification time, even while using those very tools as reachability subroutines. △ Less

Submitted 2 March, 2021; v1 submitted 20 November, 2020; originally announced November 2020.

SkyTrakx: A Toolkit for Simulation and Verification of Unmanned Air-Traffic Management Systems (Extended Version)

Authors: Chiao Hsieh, Hussein Sibai, Hebron Taylor, Yifeng Ni, Sayan Mitra

Abstract: The key concept for safe and efficient traffic management for Unmanned Aircraft Systems (UAS) is the notion of operation volume (OV). An OV is a 4-dimensional block of airspace and time, which can express an aircraft's intent, and can be used for planning, de-confliction, and traffic management. While there are several high-level simulators for UAS Traffic Management (UTM), we are lacking a framew… ▽ More The key concept for safe and efficient traffic management for Unmanned Aircraft Systems (UAS) is the notion of operation volume (OV). An OV is a 4-dimensional block of airspace and time, which can express an aircraft's intent, and can be used for planning, de-confliction, and traffic management. While there are several high-level simulators for UAS Traffic Management (UTM), we are lacking a framework for creating, manipulating, and reasoning about OVs for heterogeneous air vehicles. In this paper, we address this and present SkyTrakx -- a software toolkit for simulation and verification of UTM scenarios based on OVs. First, we illustrate a use case of SkyTrakx by presenting a specific air traffic coordination protocol. This protocol communicates OVs between participating aircraft and an airspace manager for traffic routing. We show how existing formal verification tools, Dafny and Dione, can assist in automatically checking key properties of the protocol. Second, we show how the OVs can be computed for heterogeneous air vehicles like quadcopters and fixed-wing aircraft using another verification technique, namely reachability analysis. Finally, we show that SkyTrakx can be used to simulate complex scenarios involving heterogeneous vehicles, for testing and performance evaluation in terms of workload and response delays analysis. Our experiments delineate the trade-off between performance and workload across different strategies for generating OVs. △ Less

Submitted 11 July, 2021; v1 submitted 9 September, 2020; originally announced September 2020.

Comments: 11 pages, 11 figures; This is the extended version of the paper with the same title accepted by the 24th IEEE International Conference on Intelligent Transportation (ITSC 2021)

Symmetry Abstractions for Hybrid Systems and their Applications

Authors: Hussein Sibai, Sayan Mitra

Abstract: A symmetry of a dynamical system is a map that transforms one trajectory to another trajectory. We introduce a new type of abstraction for hybrid automata based on symmetries. The abstraction combines different modes in a concrete automaton A, whose trajectories are related by symmetries, into a single mode in the abstract automaton B. The abstraction sets the guard and reset of an abstract edge t… ▽ More A symmetry of a dynamical system is a map that transforms one trajectory to another trajectory. We introduce a new type of abstraction for hybrid automata based on symmetries. The abstraction combines different modes in a concrete automaton A, whose trajectories are related by symmetries, into a single mode in the abstract automaton B. The abstraction sets the guard and reset of an abstract edge to be the union of the symmetry-transformed guards and resets of the concrete edges. We establish the soundness of the abstraction using a forward simulation relation (FSR) and present several examples. Our abstraction results in simpler automata, that are more amenable for formal analysis and design. We illustrate an application of this abstraction in making reachability analysis faster and enabling unbounded time safety verification. We show how a fixed point of the reachable set computation of B can be used to answer reachability queries for A, even if the latter visits an infinite and unbounded sequences of modes. We present our implementation of the abstraction construction, the fixed point check, and the map that transforms abstract reachable sets to concrete ones in a software tool. Finally, we show the advantage of our method over existing ones, and the different aspects of our abstraction, in a sequence of experiments including scenarios with linear and nonlinear agents following waypoints. △ Less

Submitted 16 June, 2020; originally announced June 2020.

Differentially Private Algorithms for Statistical Verification of Cyber-Physical Systems

Authors: Yu Wang, Hussein Sibai, Mark Yen, Sayan Mitra, Geir E. Dullerud

Abstract: Statistical model checking is a class of sequential algorithms that can verify specifications of interest on an ensemble of cyber-physical systems (e.g., whether 99% of cars from a batch meet a requirement on their energy efficiency). These algorithms infer the probability that given specifications are satisfied by the systems with provable statistical guarantees by drawing sufficient numbers of i… ▽ More Statistical model checking is a class of sequential algorithms that can verify specifications of interest on an ensemble of cyber-physical systems (e.g., whether 99% of cars from a batch meet a requirement on their energy efficiency). These algorithms infer the probability that given specifications are satisfied by the systems with provable statistical guarantees by drawing sufficient numbers of independent and identically distributed samples. During the process of statistical model checking, the values of the samples (e.g., a user's car energy efficiency) may be inferred by intruders, causing privacy concerns in consumer-level applications (e.g., automobiles and medical devices). This paper addresses the privacy of statistical model checking algorithms from the point of view of differential privacy. These algorithms are sequential, drawing samples until a condition on their values is met. We show that revealing the number of the samples drawn can violate privacy. We also show that the standard exponential mechanism that randomizes the output of an algorithm to achieve differential privacy fails to do so in the context of sequential algorithms. Instead, we relax the conservative requirement in differential privacy that the sensitivity of the output of the algorithm should be bounded to any perturbation for any data set. We propose a new notion of differential privacy which we call expected differential privacy. Then, we propose a novel expected sensitivity analysis for the sequential algorithm and proposed a corresponding exponential mechanism that randomizes the termination time to achieve the expected differential privacy. We apply the proposed mechanism to statistical model checking algorithms to preserve the privacy of the samples they draw. The utility of the proposed algorithm is demonstrated in a case study. △ Less

Submitted 27 June, 2022; v1 submitted 1 April, 2020; originally announced April 2020.

Comments: Under review for IEEE Open Journal of Control Systems

Multi-Agent Safety Verification using Symmetry Transformations

Authors: Hussein Sibai, Navid Mokhlesi, Chuchu Fan, Sayan Mitra

Abstract: We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map solutions and to other solutions. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of virtual system which define symmetry transformations… ▽ More We show that symmetry transformations and caching can enable scalable, and possibly unbounded, verification of multi-agent systems. Symmetry transformations map solutions and to other solutions. We show that this property can be used to transform cached reachsets to compute new reachsets, for hybrid and multi-agent models. We develop a notion of virtual system which define symmetry transformations for a broad class of agent models that visit waypoint sequences. Using this notion of virtual system, we present a prototype tool CacheReach that builds a cache of reachtubes for this system, in a way that is agnostic of the representation of the reachsets and the reachability analysis subroutine used. Our experimental evaluation of CacheReach shows up to 66% savings in safety verification computation time on multi-agent systems with 3-dimensional linear and 4-dimensional nonlinear fixed-wing aircraft models following sequences of waypoints. These savings and our theoretical results illustrate the potential benefits of using symmetry-based caching in the safety verification of multi-agent systems. △ Less

Submitted 1 November, 2019; originally announced November 2019.

Online monitoring for safe pedestrian-vehicle interactions

Authors: Peter Du, Zhe Huang, Tianqi Liu, Ke Xu, Qichao Gao, Hussein Sibai, Katherine Driggs-Campbell, Sayan Mitra

Abstract: 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 monitori… ▽ More 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 formal guarantees 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 scheme that formally assesses the safety of these interactions with nearly real-time performance (approximately 0.3 seconds). These techniques are integrated on a test vehicle with a complete in-house autonomous stack, demonstrating effective and safe interaction in real-world experiments. △ Less

Submitted 17 July, 2020; v1 submitted 12 October, 2019; originally announced October 2019.

Comments: 15 pages, 5 figures,

Adversarial Examples that Fool Detectors

Authors: Jiajun Lu, Hussein Sibai, Evan Fabry

Abstract: An adversarial example is an example that has been adjusted to produce a wrong label when presented to a system at test time. To date, adversarial example constructions have been demonstrated for classifiers, but not for detectors. If adversarial examples that could fool a detector exist, they could be used to (for example) maliciously create security hazards on roads populated with smart vehicles… ▽ More An adversarial example is an example that has been adjusted to produce a wrong label when presented to a system at test time. To date, adversarial example constructions have been demonstrated for classifiers, but not for detectors. If adversarial examples that could fool a detector exist, they could be used to (for example) maliciously create security hazards on roads populated with smart vehicles. In this paper, we demonstrate a construction that successfully fools two standard detectors, Faster RCNN and YOLO. The existence of such examples is surprising, as attacking a classifier is very different from attacking a detector, and that the structure of detectors - which must search for their own bounding box, and which cannot estimate that box very accurately - makes it quite likely that adversarial patterns are strongly disrupted. We show that our construction produces adversarial examples that generalize well across sequences digitally, even though large perturbations are needed. We also show that our construction yields physical objects that are adversarial. △ Less

Submitted 7 December, 2017; originally announced December 2017.

Comments: Follow up paper for adversarial stop signs. Submitted to CVPR 2018

Standard detectors aren't (currently) fooled by physical adversarial stop signs

Authors: Jiajun Lu, Hussein Sibai, Evan Fabry, David Forsyth

Abstract: An adversarial example is an example that has been adjusted to produce the wrong label when presented to a system at test time. If adversarial examples existed that could fool a detector, they could be used to (for example) wreak havoc on roads populated with smart vehicles. Recently, we described our difficulties creating physical adversarial stop signs that fool a detector. More recently, Evtimo… ▽ More An adversarial example is an example that has been adjusted to produce the wrong label when presented to a system at test time. If adversarial examples existed that could fool a detector, they could be used to (for example) wreak havoc on roads populated with smart vehicles. Recently, we described our difficulties creating physical adversarial stop signs that fool a detector. More recently, Evtimov et al. produced a physical adversarial stop sign that fools a proxy model of a detector. In this paper, we show that these physical adversarial stop signs do not fool two standard detectors (YOLO and Faster RCNN) in standard configuration. Evtimov et al.'s construction relies on a crop of the image to the stop sign; this crop is then resized and presented to a classifier. We argue that the crop** and resizing procedure largely eliminates the effects of rescaling and of view angle. Whether an adversarial attack is robust under rescaling and change of view direction remains moot. We argue that attacking a classifier is very different from attacking a detector, and that the structure of detectors - which must search for their own bounding box, and which cannot estimate that box very accurately - likely makes it difficult to make adversarial patterns. Finally, an adversarial pattern on a physical object that could fool a detector would have to be adversarial in the face of a wide family of parametric distortions (scale; view angle; box shift inside the detector; illumination; and so on). Such a pattern would be of great theoretical and practical interest. There is currently no evidence that such patterns exist. △ Less

Submitted 26 October, 2017; v1 submitted 9 October, 2017; originally announced October 2017.

Comments: Follow up for previous adversarial stop sign paper

NO Need to Worry about Adversarial Examples in Object Detection in Autonomous Vehicles

Authors: Jiajun Lu, Hussein Sibai, Evan Fabry, David Forsyth

Abstract: It has been shown that most machine learning algorithms are susceptible to adversarial perturbations. Slightly perturbing an image in a carefully chosen direction in the image space may cause a trained neural network model to misclassify it. Recently, it was shown that physical adversarial examples exist: printing perturbed images then taking pictures of them would still result in misclassificatio… ▽ More It has been shown that most machine learning algorithms are susceptible to adversarial perturbations. Slightly perturbing an image in a carefully chosen direction in the image space may cause a trained neural network model to misclassify it. Recently, it was shown that physical adversarial examples exist: printing perturbed images then taking pictures of them would still result in misclassification. This raises security and safety concerns. However, these experiments ignore a crucial property of physical objects: the camera can view objects from different distances and at different angles. In this paper, we show experiments that suggest that current constructions of physical adversarial examples do not disrupt object detection from a moving platform. Instead, a trained neural network classifies most of the pictures taken from different distances and angles of a perturbed image correctly. We believe this is because the adversarial property of the perturbation is sensitive to the scale at which the perturbed picture is viewed, so (for example) an autonomous car will misclassify a stop sign only from a small range of distances. Our work raises an important question: can one construct examples that are adversarial for many or most viewing conditions? If so, the construction should offer very significant insights into the internal representation of patterns by deep networks. If not, there is a good prospect that adversarial examples can be reduced to a curiosity with little practical impact. △ Less

Submitted 11 July, 2017; originally announced July 2017.

Comments: Accepted to CVPR 2017, Spotlight Oral Workshop