We present a neural network verification toolbox to 1) assess the probability of satisfaction of a constraint, and 2) modify the set to achieve the probability of satisfaction. Specifically, the tool box establishes with a user-specified level of confidence whether the output of the neural network for a given input distribution is likely to be contained within a given set. Should the tool determine that the given set cannot satisfy the likelihood constraint, the tool also implements an approach outlined in this paper to alter the set to ensure that the user-defined satisfaction probability is achieved. The toolbox is comprised of sampling-based approaches which exploit the properties of signed distance function to define set containment.

Partially autonomous driving systems may require the human driver to take control at any moment, yet by their design, they often cause difficulty with attention management. In this preliminary study, we propose a data- and dynamics-driven approach to characterize driving performance in a partially autonomous vehicle during a manual braking event, under attentive or mind wandering states. A 10-participant experiment was completed in an advanced driving simulator. We employ a non-parametric learning technique, conditional distribution embeddings, to the driving simulator data, to evaluate likelihood of successfully completing the braking maneuver, under both attentive and mind wandering states. Our approach shows a statistically significant difference in braking profiles during mind wandering and non-mind wandering episodes for each participant. Our results reveal that heterogeneity in driving performance may have important implications for the design of autonomy that is responsive to attentional states. Data-driven tools, such as the one proposed here, may be useful in designing participant-specific alerts and warnings for control handovers and other safety-critical maneuvers, because of their potential to accommodate heterogeneous response.

We present SOCKS, a data-driven stochastic optimal control toolbox based in kernel methods. SOCKS is a collection of data-driven algorithms that compute approximate solutions to stochastic optimal control problems with arbitrary cost and constraint functions, including stochastic reachability, which seeks to determine the likelihood that a system will reach a desired target set while respecting a set of pre-defined safety constraints. Our approach relies upon a class of machine learning algorithms based in kernel methods, a nonparametric technique which can be used to represent probability distributions in a high-dimensional space of functions known as a reproducing kernel Hilbert space. As a nonparametric technique, kernel methods are inherently data-driven, meaning that they do not place prior assumptions on the system dynamics or the structure of the uncertainty. This makes the toolbox amenable to a wide variety of systems, including those with nonlinear dynamics, black-box elements, and poorly characterized stochastic disturbances. We present the main features of SOCKS and demonstrate its capabilities on several benchmarks.

The articles in this special section are based on selected papers presented at the 2021 ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS 2021), a premier single-track conference that promotes development of fundamental principles that underpin the integration of cyber and physical elements, as well as the development of technologies, tools, architectures, and infrastructure for the design and implementation of CPS. ICCPS 2021 focused on contributions related to smart and connected cities, autonomous CPS, verification and control, security and privacy, and human health and biomedical CPS.

In this paper an Unmanned Aerial Vehicles (UAVs) - enabled dynamic multi-target tracking and data collection framework is presented. Initially, a holistic reputation model is introduced to evaluate the targets' potential in offloading useful data to the UAVs. Based on this model, and taking into account UAVs and targets tracking and sensing characteristics, a dynamic intelligent matching between the UAVs and the targets is performed. In such a setting, the incentivization of the targets to perform the data offloading is based on an effort-based pricing that the UAVs offer to the targets. The emerging optimization problem towards determining each target's optimal amount of offloaded data and the corresponding effort-based price that the UAV offers to the target, is treated as a Stackelberg game between each target and the associated UAV. The properties of existence, uniqueness and convergence to the Stackelberg Equilibrium are proven. Detailed numerical results are presented highlighting the key operational features and the performance benefits of the proposed framework.

We present SReachTools, an open-source MATLAB toolbox for performing stochastic reachability of linear, potentially time-varying, discrete-time systems that are perturbed by a stochastic disturbance. The toolbox addresses the problem of stochastic reachability of a target tube, which also encompasses the terminal-time hitting reach-avoid and viability problems. The stochastic reachability of a target tube problem maximizes the likelihood that the state of a stochastic system will remain within a collection of time-varying target sets for a give time horizon, while respecting the system dynamics and bounded control authority. SReachTools implements several new algorithms based on convex optimization, computational geometry, and Fourier transforms, to efficiently compute over- and under-approximations of the stochastic reach set. SReachTools can be used to perform probabilistic verification of closed-loop systems and can also perform controller synthesis via open-loop, affine, and state-feedback controllers. The code base is available online at https://github.com/unm-hscl/SReachTools, and it is designed to be extensible and user friendly.

In this demo, we present SReachTools, an open-source MATLAB toolbox for performing stochastic reachability of linear, potentially time-varying, discrete-time systems that are perturbed by a stochastic disturbance [8]. The toolbox addresses the problem of stochastic reachability of a target tube, which also encompasses the terminal-time hitting reach-avoid [7] and viability problems [1]. As illustrated in Figure 1, the stochastic reachability of a target tube problem maximizes the likelihood that the state of a stochastic system will remain within a collection of time-varying target sets for a give time horizon, while respecting the system dynamics and bounded control authority [9]. We are interested in the computation of the stochastic reach set, denoted by LSR(α), which is the set of initial states that satisfy the reach/safety specification with a likelihood above α, and the associated optimal, admissible controller.

We present a scalable algorithm to construct a polytopic underapproximation of the terminal hitting time stochastic reach-avoid set, for the verification of high-dimensional stochastic LTI systems with arbitrary stochastic disturbance. We prove the existence of a polytopic underapproximation by characterizing the sufficient conditions under which the stochastic reach-avoid set and the proposed open-loop underapproximation are compact and convex. We construct the polytopic underapproximation by formulating and solving a series of convex optimization problems. These set-theoretic properties also characterize circumstances under which the stochastic reach-avoid problem admits a bang-bang optimal Markov policy. We demonstrate the scalability of our algorithm on a 40D chain of integrators, the highest dimensional example demonstrated to date for stochastic reach-avoid problems, and compare its performance with existing approaches on a spacecraft rendezvous and docking problem.

We propose a scalable method for forward stochastic reachability analysis for uncontrolled linear systems with affine disturbance. Our method uses Fourier transforms to efficiently compute the forward stochastic reach probability measure (density) and the forward stochastic reach set. This method is applicable to systems with bounded or unbounded disturbance sets. We also examine the convexity properties of the forward stochastic reach set and its probability density. Motivated by the problem of a robot attempting to capture a stochastically moving, non-adversarial target, we demonstrate our method on two simple examples. Where traditional approaches provide approximations, our method provides exact analytical expressions for the densities and probability of capture.

Identifying collision-free paths over long time windows in environments with stochastically moving obstacles is difficult, in part because long-term predictions of obstacle positions typically have low fidelity, and the region of possible obstacle occupancy is typically large. As a result, planning methods that are restricted to identifying paths with a low probability of collision may not be able to find a valid path. However, allowing paths with a higher probability of collision may limit detection of imminent collisions. In this paper, we present Dynamic Risk Tolerance (DRT), a framework that dynamically evaluates risk tolerance, a function which is formulated as a time-varying upper bound on the acceptable likelihood of collision for a given path. DRT is implemented with forward stochastic reachable sets to predict the exact distribution of obstacles in a scalable manner over an arbitrarily long time window. In effect, DRT identifies actions that balance risks posed by both near and far obstacles. We empirically compare DRT to other state of the art methods that are capable of generating real-time solutions in highly crowded environments, and demonstrate the success rates for DRT that is 46% higher than the best performing comparison method, in the most difficult problem tested.

This study presents Busy Beeway, a mobile game platform to investigate human-automation collaboration in dynamic environments. In Busy Beeway, users collaborate with automation to evade stochastically moving obstacles and reach a series of goals, in game levels of increasing difficulty. We are motivated by the need for reliable navigation aids in stochastic, dynamic environments, which are highly relevant for self-driving vehicles, UAVs, underwater and surface vehicles, and other applications. The proposed mobile game platform is agnostic to the particular algorithm underlying the autonomous system, can be used to evaluate both fully autonomous as well as human-in-the-loop systems, and is easily deployable, for large, remote user studies. This last element is key for rigorous study of human factors in navigation aids. Through a small 32--user study, we evaluate preliminary findings regarding the relative efficacy of collaborative and fully autonomous navigation, the relationship between success rate and users' learned trust in the automation (gathered via pre- and post-experiment surveys), and tolerance to error (for decisions made by the automation and by the user). This study validates the feasibility of Busy Beeway as a platform for human subject studies on human-automation collaboration, and suggests directions for future research in human-aided planning in difficult environments.

One of the primary challenges for autonomous robotics in uncertain and dynamic environments is planning and executing a collision-free path. Hybrid dynamic obstacles present an even greater challenge as the obstacles can change dynamics without warning and potentially invalidate paths. Artificial potential field (APF)-based techniques have shown great promise in successful path planning in highly dynamic environments due to their low cost at runtime. We utilize the APF framework for runtime planning but leverage a formal validation method, Stochastic Reachable (SR) sets, to generate accurate potential fields for moving obstacles. A small number of SR sets are computed a priori, then used to generate a potential field that represents the obstacle's stochastic motion for online path planning. Our method is novel and scales well with the number of obstacles, maintaining a relatively high probability of reaching the goal without collision, as compared to other traditional Gaussian APF methods. Here, we demonstrate our method with up to 900 hybrid dynamic obstacles and show that it outperforms the traditional Gaussian APF method by up to 60% in the holonomic case and up to 20% in the unicycle case.

We present a method to validate a cognitive model, based on the cognitive architecture ACT-R, in dynamic human-automation systems with discrete human input. We are inspired by the general problem of K-choice games as a proxy for many decision making applications in dynamical systems. We model the human as a Markovian controller based on gathered experimental data, that is, a non-deterministic control input with known likelihoods of control actions associated with certain configurations of the state-space. We use reachability analysis to predict the outcome of the resulting discrete-time stochastic hybrid system, in which the outcome is defined as a function of the system trajectory. We suggest that the resulting expected outcomes can be used to validate the cognitive model against actual human subject data. We apply our method to a two-choice game in which the human is tasked with maximizing net coverage of a robotic swarm that can operate under rendezvous or deployment dynamics. We validate the corresponding ACTR cognitive model generated with the data from eight human subjects. The novelty of this work is (1) a method to compute expected outcome in a hybrid dynamical system with a Markov chain model of the human's discrete choice, and (2) application of this method to validation of cognitive models with a database of actual human subject data.

We consider hybrid systems with LTI continuous dynamics under collaborative control, that is, for which some events and inputs are controlled solely by a human operator and other events and inputs are controlled by the automation. The user-interface is a device through which the output of the system can be observed, and inputs from the human can be initiated. We model the user as an observer with additional requirements beyond a standard (automated) observer. We state conditions for user-observability and user-predictability to evaluate whether a given user-interface provides the user with adequate information to complete a desired task. We apply these conditions to two examples in aircraft flight management systems.

The papers in this special section are devoted to the topic of human-centered automation. The central theme of these papers are the tools and methods for the design and analysis of human-centered automation systems including: the design and validation of computational models of systems that integrate models of the human with models of autonomous and semi-autonomous systems; the design of systems that ease the transfer of information between humans and autonomous systems; the analysis and prediction of potential conflicts between the human and the automation in semi-autonomous systems; the design of autonomy to accommodate varying levels of human experience, training, and acuity; the analysis of information asymmetry in collaborative, semi-autonomous systems; the design of autonomy for off-nominal conditions, such as multiple sensor failures, human error, or other cascading events; and the design of autonomy to support systems with multiple humans; the design of autonomous systems which are “self-aware,” so that humans are prompted to intervene when necessary.

We consider the problem of verification of safety specifications for stochastic hybrid systems with a controller that has access to partial observations of the state. We address this problem through a finite state approximation of the stochastic hybrid system, which enables the use of existing solution techniques for partially observable Markov decision processes. First, we review a dynamic programming formulation of the safety (viability) problem over an equivalent information state. We then solve a dynamic program over the finite state approximation to generate a lower bound to the viability probability, using a point-based method that generates samples of the information state. Our approach produces approximate probabilistic viable sets and synthesizes a controller to satisfy safety specifications. We provide error bounds and convergence results, assuming additive Gaussian noise in the continuous state dynamics and observations. Finally, we demonstrate performance of the approximation on a simple temperature regulation problem.

Highly dynamic environments pose a particular challenge for motion planning due to the need for constant evaluation or validation of plans. However, due to the wide range of applications, an algorithm to safely plan in the presence of moving obstacles is required. In this paper, we propose a novel technique that provides computationally efficient planning solutions in environments with static obstacles and several dynamic obstacles with stochastic motions. Path-Guided APF-SR works by first applying a sampling-based technique to identify a valid, collision-free path in the presence of static obstacles. Then, an artificial potential field planning method is used to safely navigate through the moving obstacles using the path as an attractive intermediate goal bias. In order to improve the safety of the artificial potential field, repulsive potential fields around moving obstacles are calculated with stochastic reachable sets, a method previously shown to significantly improve planning success in highly dynamic environments. We show that Path-Guided APF-SR outperforms other methods that have high planning success in environments with 300 stochastically moving obstacles. Furthermore, planning is achievable in environments in which previously developed methods have failed.

Wireless multihop networks have a wide variety of applications, due to their rapid deployment times and minimal configuration requirements. Transmissions in wireless networks may require performance guarantees, which can be achieved by using advanced routing strategies. We examine one such performance metric, namely reliability, or packet delivery ratio in a failure-prone wireless network. We use control theoretic methods to obtain an understanding of routing in wireless multihop networks. In particular, we model ad hoc wireless networks as stochastic dynamical systems where, as a base case, a centralized controller pre-computes optimal paths to the destination. This technique can be used to obtain the highest achievable reliability for a given transmission. We compare this approach with the reliability achieved by some of the widely used routing techniques in multihop networks. We also propose extensions to the base case that can be more applicable to practical scenarios. Results show that our approach can be used to theoretically characterize reliability of end-to-end transmissions in wireless networks.

One of the many challenges in designing autonomy for operation in uncertain and dynamic environments is the planning of collision-free paths. Roadmap-based motion planning is a popular technique for identifying collision-free paths, since it approximates the often infeasible space of all possible motions with a networked structure of valid configurations. We use stochastic reachable sets to identify regions of low collision probability, and to create roadmaps which incorporate likelihood of collision. We complete a small number of stochastic reachability calculations with individual obstacles a priori. This information is then associated with the weight, or preference for traversal, given to a transition in the roadmap structure. Our method is novel, and scales well with the number of obstacles, maintaining a relatively high probability of reaching the goal in a finite time horizon without collision, as compared to other methods. We demonstrate our method on systems with up to 50 dynamic obstacles.

We present a connection between the viability kernel and maximal reachable sets. Current numerical schemes that compute the viability kernel suffer from a complexity that is exponential in the dimension of the state space. In contrast, extremely efficient and scalable techniques are available that compute maximal reachable sets. We show that under certain conditions these techniques can be used to conservatively approximate the viability kernel for possibly high-dimensional systems. We demonstrate the results on two practical examples, one of which is a seven-dimensional problem of safety in anesthesia.

We consider continuous-time LTI systems under shared control - that is, systems for which the continuous input is controlled by both a human operator and an automated-controller. The user-interface is a device through which the output of the system can be observed, and the control actions from the human can be entered. We identify observability-based conditions under which a user-interface provides the user with adequate information to accomplish a given task, formulated as a subset of the state-space. The “user-observable subspace” and the “user-predictable subspace” are calculated for two special cases: 1) when the user and the automation affect common control surfaces only, 2) when the user and the automation affect different control surfaces only. We apply our method to a real example of an aircraft accident during shared control.

Hybrid system theory lies at the intersection of the fields of engineering control theory and computer science verification. It is defined as the modeling, analysis, and control of systems that involve the interaction of both discrete state systems, represented by finite automata, and continuous state dynamics, represented by differential equations. The embedded autopilot of a modern commercial jet is a prime example of a hybrid system: the autopilot modes correspond to the application of different control laws, and the logic of mode switching is determined by the continuous state dynamics of the aircraft, as well as through interaction with the pilot. To understand the behavior of hybrid systems, to simulate, and to control these systems, theoretical advances, analyses, and numerical tools are needed. In this paper, we first present a general model for a hybrid system along with an overview of methods for verifying continuous and hybrid systems. We describe a particular verification technique for hybrid systems, based on two-person zero-sum game theory for automata and continuous dynamical systems. We then outline a numerical implementation of this technique using level set methods, and we demonstrate its use in the design and analysis of aircraft collision avoidance protocols and in verification of autopilot logic.