ABSTRACT. We address a classical identification problem that consists in estimating a vector of constant unknown parameters from a given linear input/output relationship. The estimation method that we propose relies on a network of a gradient-descent based estimators, each of which has access only to a portion of the inputs and outputs. A key feature of the approach, which stands in contrast to available literature, is that the inputs/outputs signals are allowed to be hybrid. That is, the said signals may change continuously during ordinary time, in which case we say that they {\it flow}, and they may change discretely, in which case we say that they {\it jump}, at isolated time instances. Furthermore, the different estimators exchange their estimates according to a weakly connected directed graph.

The alternation of flows and jumps combined with the distributed character of the algorithm, introduces a rich behaviour that is not possible to obtain using gradient-based estimators defined only in continuous or discrete time. Such richness is captured by a hybrid form of {\it persistence of excitation}, a condition known to be necessary for the (exponential) convergence of the estimation errors. Under this condition we establish exponential stability in a hybrid sense. Thus, the proposed approach generalizes the existing centralized gradient descent algorithms in the continuous-, the discrete-time, and the hybrid settings. In addition, we show how the proposed approach applies to an observation/identification problem for a class of uncertain high-order hybrid systems using a network of reduced-order adaptive observers/identifiers.

ABSTRACT. The mortality problem for a given dynamical system $S$ consists of determining whether every trajectory of $S$ eventually halts. In this work, we show that this problem is decidable for the class of piecewise constant derivative systems on two-dimensional manifolds, also called surfaces (\pcdm). Two closely related open problems are point-to-point and edge-to-edge reachability for \pcdm.

Building on our technique to establish decidability of mortality for \pcdm, we show that the edge-to-edge reachability problem for these systems is also decidable. In this way we solve the edge-to-edge reachability case of an open problem due to Asarin, Mysore, Pnueli and Schneider \cite{AMPS12}. This implies that the interval-to-interval version of the classical open problem of reachability for regular piecewise affine maps (PAMs) is also decidable. In other words, point-to-point reachability for regular PAMs can be effectively approximated with arbitrarily precision.

ABSTRACT. In this paper, we formulate a two-player zero-sum game under dynamic constraints given in terms of hybrid dynamical systems. We present sufficient conditions with Hamilton-Jacobi-Isaacs-like equations to guarantee attaining a solution to the game. It is shown that when the players select the optimal strategy, the value function can be evaluated without the need of computing solutions. Under additional conditions, we show that the optimal feedback laws render a set of interest asymptotically stable. Using this framework, we address an optimal control problem under the presence of an adversarial action in which the decision-making agents have dynamics that might exhibit both continuous and discrete behavior. Applications of this problem, as presented here, include disturbance rejection and security scenarios, for which the effect of the worst-case adversarial action is minimized.

ABSTRACT. In this paper, we conduct a comparison of the existing formal methods for verifying the safety of cyber-physical systems with machine learning based controllers. We focus on a particular form of machine learning based controller, namely a classifier based on multiple neural networks, the architecture of which is particularly interesting for embedded applications. We compare both exact and approximate verification techniques, based on several real-world benchmarks such as a collision avoidance system for unmanned aerial vehicles.

ABSTRACT. 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.

ABSTRACT. In this paper, we present the tool Fast Box Analysis of Two-Level Lattice Neural Networks (Fast BATLLNN) as a fast verifier of box-like output constraints for Two-Level Lattice (TLL) Neural Networks (NNs). In particular, Fast BATLLNN can verify whether the output of a given TLL NN always lies within a specified hyper-rectangle whenever its input constrained to a specified convex polytope (not necessarily a hyper-rectangle). Fast BATLLNN uses the unique semantics of the TLL architecture and the decoupled nature of box-like output constraints to dramatically improve verification performance relative to known polynomial-time verification algorithms for TLLs with generic polytopic output constraints. In this paper, we evaluate the performance and scalability of Fast BATLLNN, both in its own right and compared to state-of-the-art NN verifiers applied to TLL NNs. Fast BATLLNN compares very favorably to even the fastest NN verifiers, completing our synthetic TLL test bench more than 400x faster than its nearest competitor.