Energy consumption in buildings, both residential and commercial, accounts for approximately 40% of all energy usage in the United States, and similar numbers are being reported from countries around the world. This significant amount of energy is used to maintain a comfortable, secure, and productive environment for the occupants. So, it is crucial that energy consumption in buildings must be optimized, all the while maintaining satisfactory levels of occupant comfort, health, and safety. Machine learning (ML) has been proven to be an invaluable tool in deriving important insights from data and optimizing various systems. In this work, we review some of the most promising ways in which ML has been leveraged to make buildings smart and energy-efficient. For the convenience of readers, we provide a brief introduction to the relevant ML paradigms and the components and functioning of each smart building system we cover. Finally, we discuss the challenges faced while implementing machine learning algorithms in smart buildings and provide future avenues for research in this field.

Many of the popular reachability analysis methods rely on the existence of system models. When system dynamics are uncertain or unknown, data-driven techniques must be utilized instead. In this paper, we propose an approach to data-driven reachability that provides a probabilistic guarantee of correctness for these systems through nonconvex scenario optimization. We pose the problem of finding reachable sets directly from data as a chance-constrained optimization problem, and present two algorithms for estimating nonconvex reachable sets: (1) through the union of partition cells and (2) through the sum of radial basis functions. Additionally, we investigate numerical examples to demonstrate the capability and applicability of the introduced methods to provide nonconvex reachable set approximations.

Gaussian process state space models are becoming common tools for the analysis and design of nonlinear systems with uncertain dynamics. When designing control policies for these systems, safety is an important property to consider. In this paper, we provide safety guarantees for Gaussian process state space models in the form of probabilistic invariant sets, where the state trajectory is guaranteed to lie within an invariant set for all time with a particular probability. We provide a sufficient condition in the form of a linear matrix inequality to evaluate the probabilistic invariance of the system, and we demonstrate our contributions with an illustrative example.

Complex-valued Gaussian processes are used in Bayesian frequency-domain system identification as prior models for regression. If each realization of such a process were an $H_\infty$ function with probability one, then the same model could be used for probabilistic robust control, allowing for robustly safe learning. We investigate sufficient conditions for a general complex-domain Gaussian process to have this property. For the special case of processes whose Hermitian covariance is stationary, we provide an explicit parameterization of the covariance structure in terms of a summable sequence of nonnegative numbers.

We present algorithms for estimating the forward reachable set of a dynamical system using only a finite collection of independent and identically distributed samples. The produced estimate is the sublevel set of a function called an empirical inverse Christoffel function: empirical inverse Christoffel functions are known to provide good approximations to the support of probability distributions. In addition to reachability analysis, the same approach can be applied to general problems of estimating the support of a random variable, which has applications in data science towards detection of novelties and outliers in data sets. In applications where safety is a concern, having a guarantee of accuracy that holds on finite data sets is critical. In this paper, we prove such bounds for our algorithms under the Probably Approximately Correct (PAC) framework. In addition to applying classical Vapnik-Chervonenkis (VC) dimension bound arguments, we apply the PAC-Bayes theorem by leveraging a formal connection between kernelized empirical inverse Christoffel functions and Gaussian process regression models. The bound based on PAC-Bayes applies to a more general class of Christoffel functions than the VC dimension argument, and achieves greater sample efficiency in experiments.

Research at the interface between formal methods and control theory has given rise to symbolic control [1], [2], [3], which deals with control of dynamical systems with logic specifications. A key ingredient of symbolic control is a finite abstraction, i.e. a dynamical system with a finite number of states and inputs, also called symbolic model, constructed from the original system. When the concrete and abstract systems are related by a behavioral relation, such as an approximate alternating simulation relation [1], showing that the trajectories of the abstraction mimic the ones of the original system, the discrete controller synthesized for the abstraction can be refined into a hybrid controller for the original system.

This chapter applies interval reachability analysis to the problem of evaluating the robustness of a system against the effects of uncertain parameters. Specifically, we consider the volume of an interval reachable set as a continuous performance measure to gauge the robustness of a system, which can be used to guide the design of a robust controller. The volume of the interval over-approximation measures the effect of the parameter uncertainty on system trajectories starting in a given initial set: a smaller volume implies a smaller effect, and therefore, greater robustness. We illustrate this approach to robustness analysis on a medical exoskeleton model which has 6 states and 12 uncertain parameters. The dynamics of this system are too complicated to derive detailed system information such as bounds on the Jacobian matrix or growth bound functions, which precludes the use of the more efficient methods introduced in this book. Instead, we rely on the computationally expensive but widely applicable sampling-based methods on sampled-data mixed monotonicity and the Monte Carlo approach.

ion-based control synthesis is a three-step process to solve a control problem for continuous-state system (difference equation or differential equation), by first abstracting this system into a finite transition system, solving the control problem on the abstraction, and finally refining the obtained controller to apply it to the continuous system. This chapter first provides an overview of the three steps of abstraction-based approaches and on the key role played by reachability analysis in the first step to create the finite abstraction. This approach is then illustrated on a docking problem for a marine vessel corresponding to a reach-avoid specification (reach the docking area in finite time while avoiding obstacles). This example highlights how the forward reachability analysis methods presented in this book can be used within such abstraction-based approaches to solve backward reachability problems.

This chapter applies the discrete-time mixed-monotonicity method from the previous chapter to the sampled-data version of a continuous-time system, thus overcoming the conservativeness of the continuous-time mixed-monotonicity approach. The main difficulty arising from this approach is that the boundedness assumption on the Jacobian matrices of the discrete-time system (corresponding to the sampled-data system) is converted into a boundedness assumption on the sensitivity matrices of the continuous-time system (the partial derivative of the state trajectories with respect to the initial conditions). Since these sensitivity matrices are partial derivatives of the continuous-time trajectories whose closed-form expression is usually unknown, the satisfaction of this assumption requires significant effort. We thus provide three methods to compute bounds on the sensitivity matrix: using interval analysis on the dynamics of the sensitivity matrix; approximating this bound through a sampling-based approach; and a hybrid version of the previous two methods resulting in a sound over-approximation with a tunable tradeoff between its conservativeness and computational complexity.

Symbolic control techniques aim to satisfy complex logic specifications. A critical step in these techniques is the construction of a symbolic (discrete) abstraction, a finite-state system whose behaviour mimics that of a given continuous-state system. The methods used to compute symbolic abstractions, however, require knowledge of an accurate closed-form model. To generalize them to systems with unknown dynamics, we present a new data-driven approach that does not require closed-form dynamics, instead relying only the ability to evaluate successors of each state under given inputs. To provide guarantees for the learned abstraction, we use the Probably Approximately Correct (PAC) statistical framework. We first introduce a PAC-style behavioural relationship and an appropriate refinement procedure. We then show how the symbolic abstraction can be constructed to satisfy this new behavioural relationship. Moreover, we provide PAC bounds that dictate the number of data required to guarantee a prescribed level of accuracy and confidence. Finally, we present an illustrative example.

Reachability analysis is used to determine all possible states that a system acting under uncertainty may reach. It is a critical component to obtain guarantees of various safety-critical systems both for safety verification and controller synthesis. Though traditional approaches to reachability analysis provide formal guarantees of the reachable set, they involve complex algorithms that require full system information, which is impractical for use in real world settings. We present DaDRA, a Python library that allows for data-driven reachability analysis with arbitrarily robust probabilistic guarantees. We demonstrate the practical functionality of DaDRA on various systems including: an analytically intractable chaotic system, benchmarks for systems with nonlinear dynamics, and a realistic system acting under complex disturbance signals and controlled with an intricate controller across multiple dimensions.

In this chapter, we consider reachability methods that characterize how a set centered around a system trajectory grows or contracts as the trajectory evolves. In particular, we consider interval growth bounds, which characterize the growth and contraction of intervals. An interval over-approximation of the reachable set from an interval of initial states can be obtained by computing a single successor state from the center of the initial set and bounding the growth of neighboring trajectories. We first describe the general method for over-approximating reachable sets with interval growth bounds. Then, we describe three methods to compute such growth bounds: from a matrix measure of the state Jacobian matrix; from a componentwise upper bound on the state Jacobian matrix; and from matrix measures of a blockwise partition of the state Jacobian matrix to allow for a greater flexibility in computational efficiency and conservativeness.

The computation of reachable sets is an effective way to characterize and verify the behavior of safety-critical cyber-physical systems. However, many systems of practical interest possess high-dimensional, analytically intractable, and possibly unknown dynamics, which make the computation of safe sets with formal guarantees difficult or impossible. In these cases we can employ a data-driven approach to reachability analysis instead. The data-driven approach uses a finite ensemble of sample trajectories to compute reachable set estimates which are guaranteed to achieve high accuracy in a probabilistic sense.

This chapter considers methods that compute reachable set approximations by evaluating the successor function on a finite set of sample points. Such sampling-based methods can work under mild system assumptions for both continuous-time and discrete-time systems, but they require the successor function to be evaluated once for each sample point. Sampling-based methods are, therefore, broadly applicable and also computationally expensive. The first sampling-based method presented in this chapter constructs a grid over the initial states and inputs, evaluates the successor state of each grid point, and expands the interval hull of these successors by an error bound to obtained a reachable set over-approximation. Due to the grid-based sampling scheme, the number of sample points used by this quasi-Monte Carlo method increases exponentially with the state and input dimensions. To avoid the exponential scaling, the second method uses a randomized sampling scheme. Due to its probabilistic nature, this Monte Carlo method is not guaranteed to over-approximate the reachable set. However, it can produce an approximation which is close to the reachable set in a probabilistic sense, and the required number of samples increases only linearly in the state dimension.

We present an algorithm for data-driven reachability analysis that estimates finite-horizon forward reachable sets for general nonlinear systems using sub-level sets of a certain class of polynomials known as empirical inverse Christoffel functions, which are known empirically to provide good approximations to the support of probability distributions. The algorithm uses this property for reachability analysis by solving a probabilistic relaxation of the reachable set computation problem. We also provide a guarantee that the output of the algorithm is an accurate reachable set approximation in a probabilistic sense, provided that a certain sample size is attained. We also investigate three numerical examples to demonstrate the algorithm’s capabilities, such as providing non-convex reachable set approximations and detecting holes in the reachable set.

Despite their efficiency and guaranteed tightness, the applicability of the over-approximation methods relying on the monotonicity property in the previous chapter are limited to the class of monotone systems. In this chapter, we provide generalizations of monotonicity-based methods by considering a wider class of mixed-monotone systems, which are systems whose dynamics can be embedded in an auxiliary system which is monotone. In particular, we show that the mixed-monotonicity property is satisfied by any Lipschitz continuous nonlinear system, thus making the associated reachability methods broadly applicable. We present both the continuous-time and discrete-time versions of this result.