We study distributional reachability for finite Markov decision processes (MDPs) from a control theoretical perspective. Unlike standard probabilistic reachability notions, which are defined over MDP states or trajectories, in this paper reachability is formulated over the space of probability distributions. We propose two set-valued maps for the forward and backward distributional reachability problems: the forward map collects all state distributions that can be reached from a set of initial distributions, while the backward map collects all state distributions that can reach a set of final distributions. We show that there exists a maximal invariant set under the forward map and this set is the region where the state distributions eventually always belong to, regardless of the initial state distribution and policy. The backward map provides an alternative way to solve a class of important problems for MDPs: the study of controlled invariance, the characterization of the domain of attraction, and reach-avoid problems. Three case studies illustrate the effectiveness of our approach.

This article proposes a solution to the overtaking control problem where an automated vehicle tries to overtake another vehicle with uncertain motion. Our solution allows the automated vehicle to robustly overtake a human-driven vehicle under certain assumptions. Uncertainty in the predicted motion makes the automated overtaking problem hard to solve due to feasibility issues that arise from the fact that the overtaken vehicle (e.g., a vehicle driven by an aggressive driver) may accelerate to prevent the overtaking maneuver. To counteract them, we introduce the weak assumption that the predicted velocity of the overtaken vehicle respects a supermartingale, meaning that its velocity is not increasing in expectation during the maneuver. We show that this formulation presents a natural notion of risk. Based on the martingale assumption, we perform a risk-aware reachability analysis by analytically characterizing the predicted collision probability. Then, we design a risk-aware optimal overtaking algorithm with guaranteed levels of collision avoidance. Finally, we illustrate the effectiveness of the proposed algorithm with a simulated example. 

We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct temporal logic trees (TLT) from LTL formulae via reachability analysis. In contrast to automaton-based methods, the construction of the TLT is abstraction-free for infinite systems, that is, we do not construct discrete abstractions of the infinite systems. Moreover, for a given transition system and an LTL formula, we prove that there exist both a universal TLT and an existential TLT via minimal and maximal reachability analysis, respectively. We show that the universal TLT is an underapproximation for the LTL formula and the existential TLT is an overapproximation. We provide sufficient conditions and necessary conditions to verify whether a transition system satisfies an LTL formula by using the TLT approximations. As a major contribution of this work, for a controlled transition system and an LTL formula, we prove that a controlled TLT can be constructed from the LTL formula via control-dependent reachability analysis. Based on the controlled TLT, we design an online control synthesis algorithm, under which a set of feasible control inputs can be generated at each time step. We also prove that this algorithm is recursively feasible. We illustrate the proposed methods for both finite and infinite systems and highlight the generality and online scalability with two simulated examples.

This article investigates stochastic invariance for control systems through probabilistic controlled invariant sets (PCISs). As a natural complement to robust controlled invariant sets (RCISs), we propose finite-, and infinite-horizon PCISs, and explore their relation to RICSs. We design iterative algorithms to compute the PCIS within a given set. For systems with discrete spaces, the computations of the finite-, and infinite-horizon PCISs at each iteration are based on linear programming, and mixed integer linear programming, respectively. The algorithms are computationally tractable, and terminate in a finite number of steps. For systems with continuous spaces, we show how to discretize the spaces, and prove the convergence of the approximation when computing the finite-horizon PCISs. In addition, it is shown that an infinite-horizon PCIS can be computed by the stochastic backward reachable set from the RCIS contained in it. These PCIS algorithms are applicable to practical control systems. Simulations are given to illustrate the effectiveness of the theoretical results for motion planning.

An invariant cover quantifies the information needed by a controller to enforce an invariance specification. This paper investigates some fundamental problems concerning existence and computation of an invariant cover for uncertain discrete-time linear control systems subject to state and control constraints. We develop necessary and sufficient conditions on the existence of an invariant cover for a polytopic set of states. The conditions can be checked by solving a set of linear programs, one for each extreme point of the state set. Based on these conditions, we give upper and lower bounds on the minimal cardinality of the invariant cover, and design an iterative algorithm with finite-time convergence to compute an invariant cover. We further show in two examples how to use an invariant cover in the design of a coder-controller pair that ensures invariance of a given set for a networked control system with a finite communication data rate.

An adaptive interpolating control (AIC) algorithm is proposed for constrained linear systems with parametric uncertainty and additive disturbance. This adaptive algorithm consists of an iterative set membership identification algorithm, which updates the uncertain parameter set at each time step, and an interpolating controller, which robustly stabilizes the uncertain system with state and input constraints. We prove that the AIC algorithm is recursively feasible and guarantees robust constraint satisfaction and robust asymptotic stability of the closed-loop system in the presence of uncertainties. Moreover, we detail two possible extensions of the AIC algorithm: (a) persistent excitation conditions can be embedded into the AIC algorithm to accelerate the convergence of system parameters and (b) the combination of the AIC algorithm and aggressive learning is able to enlarge the size of the feasible region with every iteration by exploiting information from previous iterations. We illustrate the effectiveness of the proposed algorithms through comparisons with adaptive model predictive control and one example of mobile carrier robot.

In this paper, we propose an approach for ensuring the safety of a vehicle throughout a parking task, even when the vehicle is being operated at varying levels of automation. We start by specifying a vehicle parking task using linear temporal logic formulae that can be model checked for feasibility. The model-checking is facilitated by the construction of a temporal logic tree via Hamilton-Jacobi reachability analysis. Once we know the parking task is feasible for our vehicle model, we utilize the constructed temporal logic tree to directly synthesize control sets. Our approach synthesizes control sets that are least-restrictive in the context of the specification, since they permit any control inputs that are guaranteed not to violate the specification. This least-restrictive characteristic allows for the application of our approach to vehicles under different modes of operation (e.g., human-in-the-loop shared autonomy or fully-automated schemes). Implementing in both simulation and on hardware, we demonstrate the approach's potential for ensuring the safety of vehicles throughout parking tasks, whether they are operated by humans or automated driving systems. 

In this paper, we propose a framework for the safe teleoperation of connected vehicles by remote human operators. The proposed framework combines model-checking, reachability analysis, and human factor design into a unified approach that checks the feasibility of linear temporal logic (LTL) specified teleoperation tasks, guarantees safety throughout the execution of the tasks, and keeps the remote operator as the primary decision maker in the control loop. We apply the general approach to a remote parking example to illustrate the framework. Then, to evaluate the framework's benefits and usability, we conduct a user study on an experimental remote control operator's room and a 1/10th scale vehicle. In the user study, we validate the approach's ability to ensure the completion of LTL-specified tasks and gain initial insight into whether human users find the teleoperation system intuitive.

This paper proposes a new notion of stabilization in probability for discrete-time stochastic systems that may be with unbounded disturbances and bounded control input. This new notion builds on two sets: target set and region of attraction. The target set is a set within which the controller is able to keep the system state with a certain probability. The region of attraction is a set from which the controller is able to drive the system state to the target set with a prescribed probability. We investigate the probabilistic characterizations of these two sets for linear stochastic control systems. We provide sufficient conditions for a compact set to be a target set with a given horizon and probability level. Given a target set, we use two methods to characterize the region of attraction: one is based on the solution to a stochastic optimal first-entry time problem while the other is based on stochastic backward reachable sets. For linear scalar systems, we provide analytic representations for the target set and the region of attraction. Simulations are given to illustrate the effectiveness of the theoretical results.

We propose a shared autonomy approach for implementing human operator decisions onto an automated system during multi-objective missions, while guaranteeing safety and mission completion. A mission is specified as a set of linear temporal logic (LTL) formulae. Then, using a novel correspondence between LTL and reachability analysis, we synthesize a set of controllers for assisting the human operator to complete the mission, while guaranteeing that the system maintains specified spatial and temporal properties. We assume the human operator's exact preference of how to complete the mission is unknown. Instead, we use a datadriven approach to infer and update the automated system's internal belief of which specified objective the human intends to complete. If, while the human is operating the system, she provides inputs that violate any of the invariances prescribed by the LTL formula, our verified controller will use its internal belief of the human operator's intended objective to guide the operator back on track. Moreover, we show that as long as the specifications are initially feasible, our controller will stay feasible and can guide the human to complete the mission despite some unexpected human errors. We illustrate our approach with a simple, but practical, experimental setup where a remote operator is parking a vehicle in a parking lot with multiple parking options. In these experiments, we show that our approach is able to infer the human operator's preference over parking spots in real-time and guarantee that the human will park in the spot safely.