ABSTRACT. Barrier certificates provide safety guarantees for hybrid systems. In this paper, we propose a novel approach to synthesize neural networks as barrier certificates. Candidate networks are trained from a special structure: ReLU neural networks consisting of two hidden layers. Then, the problem of identifying real barrier certificates from candidates is transformed into a group of mixed integer linear programming problems and a mixed integer quadratically constrained problem. Taking full advantage of the recent advance in optimization, barrier certificates validation can be performed effectively. We implement the tool SyntheBC and evaluate its performance over 3 hybrid systems and 8 continuous systems up to 12-dimensional state space. The experimental results show that our method is more scalable and effective than the classical polynomial barrier certificate method and the existing neural network based method.

ABSTRACT. We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal abstraction of the switched system in terms of an uncertain Markov model, namely an Interval Markov Decision Process (IMDP), by accounting for both the stochastic behavior of the system and the uncertainty in the learning step. We synthesize a strategy on the resulting IMDP that maximizes the satisfaction probability of the LTLf specification and is robust against all the uncertainties in the abstraction. This strategy is then refined into a switching strategy for the original stochastic system. We show that this strategy is near-optimal and provide a bound on its distance (error) to the optimal strategy. We experimentally validate our framework on various case studies, including both linear and non-linear switched stochastic systems. This work makes a step towards the development of provably correct data-driven autonomous systems.

ABSTRACT. We introduce OmegaThreads, a software tool for automatic synthesis of correct-by-construction controllers for control systems from $\omega$-regular specifications. It accepts general nonlinear control systems from which discrete abstractions (a.k.a. symbolic models) are constructed. Specifications are provided directly as deterministic parity Automata (DPA) or as linear temporal logic (LTL) formulae which are used to construct the corresponding DPAs. OmegaThreads constructs a two-player parity game from a symbolic model and a DPA. Then, it searches for a winning strategy playing as a controller against the symbolic model. If exists, OmegaThreads extracts the winning strategy as a Mealy machine.

OmegaThreads is implemented in C++ and OpenCL on top of pFaces, a recently introduced acceleration ecosystem. Inputs are given as text configuration files written in simple language. A Python interface is developed to access the synthesized Mealy machines. A 2D simulator is provided to simulate the closed-loop behaviour of the control system equipped with the synthesized controller. Two examples are presented: motion planning for an autonomous vehicle and mission planning for a drone operated on a battery.

ABSTRACT. Reachability analysis fails to produce tight reachable sets if certain algorithm parameters are poorly tuned, such as the time step size or the accuracy of the set representation. The tuning is especially difficult in the context of nonlinear systems where over-approximation errors accumulate over time due to the so-called wrapping effect, often requiring expert knowledge. In order to widen the applicability of reachability analysis for practitioners, we propose the first adaptive parameter tuning approach for reachability analysis of nonlinear continuous systems tuning all algorithm parameters. Our modular approach can be applied to different reachability algorithms as well as various set representations. Finally, an evaluation on numerous benchmark systems shows that the adaptive parameter tuning approach efficiently computes very tight enclosures of reachable sets.

ABSTRACT. We consider the decidability of state-to-state reachability in linear time-invariant control systems over continuous time. We analyse this problem with respect to the allowable control sets, which are assumed to be the image under a linear map of the unit hypercube (\emph{i.e.} zonotopes). This naturally models bounded (sometimes called saturated) controls. Decidability of the version of the reachability problem in which control sets are affine subspaces of $\mathbb{R}^n$ is a fundamental result in control theory. Our first result is decidability in two dimensions ($n=2$) if the matrix $A$ satisfies some spectral conditions, and conditional decidablility in general. If the transformation matrix $A$ is diagonal with rational entries (or rational multiples of the same algebraic number) then the reachability problem is decidable. If the transformation matrix $A$ only has real eigenvalues, the reachability problem is conditionally decidable. The time-bounded reachability problem is conditionally decidable, and unconditionally decidable in two dimensions. Some of our results rely on the decidability of certain logical theories --- namely the theory of the reals with exponential ($\mathfrak{R}_{\exp}$) and with bounded sine ($\mathfrak{R}_{\exp,\sin}$)--- which have been proven decidable conditional on Schanuel's Conjecture --- a unifying conjecture in transcendence theory. We also obtain a hardness result for a mild generalization of the problem where the target is a simple set (hypercube of dimension $n-1$ or hyperplane) instead of a point. In this case, we show that the problem is at least as hard as the \emph{Continuous Positivity problem} if the control set is a singleton, or the \emph{Nontangential Continuous Positivity problem} if the control set is $[-1,1]$.

ABSTRACT. We present a MATLAB toolbox for Automated Reachset Optimal Control (AROC) that automatically synthesizes verified controllers for solving reach-avoid problems using reachability analysis. The toolbox implements two different types of control approaches: In model predictive control a feasible controller is constructed and verified on-the-fly during online application of the system. For motion-primitive-based control, on the other hand, controllers for many motion primitives are synthesized offline and then used for online motion planning with a maneuver automaton. Since our toolbox considers general nonlinear systems with input constraints, state constraints, and bounded disturbances, it is applicable to a very broad class of systems as we demonstrate with several numerical examples.

ABSTRACT. Deep Neural Networks (DNNs) have demonstrated to be powerful machine learning models for approximating complex functions. In this work, we provide an exact reachability analysis method for DNN with Rectified Linear Unit (ReLU) activation function. At its core, our set-based method utilizes a facet-vertex incidence matrix, which represents a complete encoding of the combinatorial structure of convex sets. When a safety violation is detected, our approach provides backtracing which determines the complete input set that caused the safety violation. The performance of our method is evaluated and compared to other state-of-the-art methods by using the ACAS Xu flight controller and other benchmarks.

ABSTRACT. In this work, we consider continuous-time controlled systems with disturbances and we show how controlled robustly forward invariant sets are identified by applying the mixed-monotonicity property. A mixed-monotone system can be embedded in a related deterministic embedding system with twice as many states but for which the dynamics are monotone; the powerful theory of monotonicity can then be applied to the embedding system to conclude useful properties of the initial system. We show how feedback controllers are verified against safety (set invariance) constraints, and our approach involves a control barrier function type condition, requiring the vector field of the embedding system, when evaluated at a particular state in the embedding space, point into a certain cone. This approach facilitates the construction of runtime assurance mechanisms for controlled systems with disturbances, and we study also control system safety in the presence of state uncertainty. The results and findings of this work are demonstrated through two numerical examples where we study (i) the verification of a controlled spacecraft system against a safety constraint, and (ii) the formation of a runtime assurance mechanism that functions in the presence of uncertain state measurements.

ABSTRACT. In this paper, we present a compositional proof rule for ensuring safety of a collection of interacting systems modeled by inter-triggering hybrid automata (ITHA). ITHA is a modeling formalism to represent multi-agent systems where each agent has their individual dynamics but can also interact with other agents through triggering actions. These triggering actions result in a jump/reset in the state of other agents according to a global resolution function. The proof rule, inspired by responsibility-sensitive safety, consists of two parts: self-safety relating to individual dynamics, and responsibility relating to triggering actions and an estimate of the resolution function. We prove that observance of these two rules by each agent is sufficient for the safety of the overall collection if the resolution function estimate is an over-approximation. We further show how such over-approximations can be obtained and improved via communication. We use two examples, a job scheduling task on parallel processors and a highway driving example, throughout the paper to illustrate the concepts. Finally, we provide a comprehensive evaluation on how the proposed proof rule can be leveraged for several multi-agent control and supervision examples.