We present an approach for identifying two subclasses of piecewise affine (PWA) systems that we call flagged and guarded linear systems. Flagged linear system dynamics are given by a sum of k linear dynamical modes, each activated based on a latent binary variable, called a flag. Additionally, guarded linear systems define each flag as the sign of an affine “guard” function. We term the discovery of the latent flag values and the corresponding linear dynamics as the “flagged regression” and “guarded regression” problems, respectively. We show that the system identification problem is NP-hard even for these models, making the identification problem computationally challenging. For both problems, we provide approximation algorithms that identify a model whose error is within some user-defined constant away from the optimum. The time complexity of these algorithms is linear in the number of data points but exponential in the state-space dimension and the number of flags. The linear complexity in data size allows our approach to potentially scale to large data sets. We evaluate our algorithms on benchmark problems in order to learn models for mechanical systems with contact forces and a nonlinear robotic arm benchmark. Our approach compares favorably against neural network learning and the PARC algorithm for identifying PWA models proposed by Bemporad.

In this paper, we study the “decoding” problem for discrete-time, stochastic hybrid systems with linear dynamics in each mode. Given an output trace of the system, the decoding problem seeks to construct a sequence of modes and states that yield a trace “as close as possible” to the original output trace. The decoding problem generalizes the state estimation problem, and is applicable to hybrid systems with non-determinism. The decoding problem is NP-complete, and can be reduced to solving a mixed-integer linear program (MILP). In this paper, we decompose the decoding problem into two parts: (a) finding a sequence of discrete modes and transitions; and (b) finding corresponding continuous states for the mode/transition sequence. In particular, once a sequence of modes/transitions is fixed, the problem of “filling in” the continuous states is performed by a linear programming problem. In order to support the decomposition, we “cover” the set of all possible mode/transition sequences by a finite subset. We use well-known probabilistic arguments to justify a choice of cover with high confidence and design randomized algorithms for finding such covers. Our approach is demonstrated on a series of benchmarks, wherein we observe that relatively tiny fraction of the possible mode/transition sequences can be used as a cover. Furthermore, we show that the resulting linear programs can be solved rapidly by exploiting the tree structure of the set cover.

This paper studies the decoding problem of discrete-time stochastic hybrid systems with linear dynamics at each mode. The problem of reconstructing the sequence of continuous states, modes, and transitions of a hybrid system given only a sequence of possibly noisy outputs is referred to as the decoding problem 1. The decoding problem is NP-complete [4] and can be reduced to solving a mixed integer linear program (MILP). In this paper, we propose a solution that solves a relaxation of the decoding problem. The approach iterates over two steps - (a) fixing the sequence of modes and transitions for the given output sequence; and (b) estimating the continuous states. To make the first part tractable, we identify a finite subset of mode/transition sequences that “covers” the set of all such possible sequences and then iterate over this subset instead. The cover is generated using randomized algorithms and justified using well-known probabilistic arguments with high confidence. We demonstrate the proposed approach on a set of seven benchmarks. We observe that a relatively tiny subset of all possible mode/transition sequences suffices as a cover and the proposed approach solves the resulting state estimation problem rapidly by utilizing a tree data structure.

We present an algorithm for learning switched linear dynamical systems in discrete time from noisy observations of the system's full state or output. Switched linear systems use multiple linear dynamical modes to fit the data within some desired tolerance. They arise quite naturally in applications to robotics and cyber-physical systems. Learning switched systems from data is a NP-hard problem that is nearly identical to the $k$-linear regression problem of fitting $k > 1$ linear models to the data. A direct mixed-integer linear programming (MILP) approach yields time complexity that is exponential in the number of data points. In this paper, we modify the problem formulation to yield an algorithm that is linear in the size of the data while remaining exponential in the number of state variables and the desired number of modes. To do so, we combine classic ideas from the ellipsoidal method for solving convex optimization problems, and well-known oracle separation results in non-smooth optimization. We demonstrate our approach on a set of microbenchmarks and a few interesting real-world problems. Our evaluation suggests that the benefits of this algorithm can be made practical even against highly optimized off-the-shelf MILP solvers.

We introduce Meta-F $$^{\star }$$ , a tactics and metaprogramming framework for the F $$^\star $$ program verifier. The main novelty of Meta-F $$^\star $$ is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F $$^\star $$ can be used to generate verified code automatically. Meta-F $$^\star $$ is implemented as an F $$^\star $$ effect, which, given the powerful effect system of F $$^{\star }$$ , heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F $$^\star $$ type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F $$^\star $$ provides substantial gains in proof development, efficiency, and robustness.

Neural networks are increasingly used as data-driven models for a wide variety of physical systems such as ground vehicles, airplanes, human physiology and automobile engines. These models are in-turn used for designing and verifying autonomous systems. The advantages of using neural networks include the ability to capture characteristics of particular systems using the available data. This is particularly advantageous for medical systems, wherein the data collected from individuals can be used to design devices that are well-adapted to a particular individual's unique physiological characteristics. At the same time, neural network models remain opaque: their structure makes them hard to understand and interpret by human developers. One key challenge lies in checking that neural network models of processes are “conformant” to the well established scientific (physical, chemical and biological) laws that underlie these models. In this paper, we will show how conformance often fails in models that are otherwise accurate and trained using the best practices in machine learning, with potentially serious consequences. We motivate the need for learning and verifying key conformance properties in data-driven models of the human insulin-glucose system and data-driven automobile models. We survey verification approaches for neural networks that can hold the key to learning and verifying conformance.