ABSTRACT. Safety verification is an essential requirement of neural network controlled systems when they are adopted in safety-critical fields. This paper proposes a novel approach to synthesizing neural networks as barrier certificates, which can provide safety guarantees for neural network controlled systems. We first propose the construction conditions of neural network barrier certificates, followed by an iterative framework to synthesize them. Each iteration trains a neural network as the candidate barrier certificate using the training datasets sampled from the neural network controlled system. After training, identifying whether the candidate barrier certificate is a real one for the neural network controlled system is transformed into a group of mixed-integer programming problems, which the numerical optimization solver solves with guaranteed results. We implement the tool NetBC and evaluate its performance over 6 practical benchmark examples. The experimental results show that NetBC is more effective and scalable than the existing polynomial barrier certificate-based method.

ABSTRACT. Piecewise linearization based reachable set computation of nonlinear systems has the advantage that reachable sets of the linear systems obtained post linearization can be computed efficiently. However, this approach suffers from curse of dimensionality because the number of pieces required to restrict the linearization error below a threshold can blow up for high-dimensional systems. Alternatively, we can fix the maximum number of divisions of the reachable set and optimize the division vector to minimize the linearization error. But the functions projecting the linearization error along different directions can be different, which have different optimal solutions for the division vector. Still, we may need to minimize the linearization error along multiple directions to achieve good accuracy along any one direction because the differential equations can be coupled. Therefore, we develop a new method of piecewise linearization based reachable set computation that incorporates different optimized divisions of reachable set for different projections of linearization error to improve accuracy. To do so, we use intersection of unions of sets (IoU) to approximate reachable sets such that different unions in the intersection are obtained from optimized division along different directions and forward propagation. We develop an algorithm to propagate the reachable set of the IoU in a coupled way, such that each intersecting union complements the approximation accuracy of other unions. We validate the advantage of using multiple optimal divisions instead of single optimized division. For this, we compare the performance on high dimensional examples, of the proposed algorithm with a variant of the algorithm which uses a single optimized division at each time step. We also draw comparison with state-of-the-art methods and demonstrate that the accuracy of our algorithm is at par or better for the benchmarks.

ABSTRACT. As the scope and complexity of modern cyber-physical systems increase, newer and more challenging mission requirements will be imposed on the optimal control of the underlying unmanned systems. This paper proposes a solution to handle complex temporal requirements formalized in Signal Temporal Logic (STL) specifications within the Successive Convexification (SCvx) algorithmic framework. This SCvx-STL solution method consists of four steps: 1) Express the STL specifications using their robust semantics as state constraints. 2) Introduce new auxiliary state variables to transform these state constraints as system dynamics, by exploiting the recursively defined structure of robust STL semantics. 3) Smooth the resulting system dynamics with polynomial smooth min- and max- functions. 4) Convexify and solve the resulting optimal control problem with the SCvx algorithm, which enjoys guaranteed convergence and polynomial time subproblem solving capability. Our approach retains the expressiveness of encoding mission requirements with STL semantics, while avoiding the usage of combinatorial optimization techniques such as Mixed-integer programming. Numerical results are shown to demonstrate its effectiveness.

ABSTRACT. We present ABS, a software for Abstraction-Based Synthesis of controllers for continuous-state control systems. The tool distin- guishes itself from previously known such software by being for- mally correct, i.e., any controller synthesized by ABS is mathemat- ically guaranteed to solve the control problem provided as input. ABS achieves this quality by providing an input language with mathematically defined semantics and a respective compiler, and by carefully taking into account all numerical and rounding errors that might be incurred at either compile- or run-time. To mitigate computational overhead caused by the aforementioned approach, ABS implements, e.g. on-the-fly synthesis algorithms with greatly reduced memory demand. The tool is currently applicable to invari- ance and reachability problems and requires state measurement. We discuss structure, algorithmic details and basic usage of ABS, and we demonstrate on two examples that its performance com- pares favorably with competing, not formally correct synthesis software. Upon acceptance of this paper for publication, the source code of ABS will be made publicly available.

ABSTRACT. We present ETCetera, a Python library developed for the analysis and synthesis of the sampling behaviour of event triggered control (ETC) systems. In particular, the tool constructs abstractions of the sampling behaviour of given ETC systems, in the form of timed automata (TA) or finite-state transition systems (FSTSs). When the abstraction is an FSTS, ETCetera provides diverse manipulation tools for analysis of ETC's sampling performance, synthesis of communication traffic schedulers (when networks shared by multiple ETC loops are considered), and optimization of sampling strategies. Additionally, the TA models may be exported to UPPAAL for analysis and synthesis of schedulers. Several examples of the tool's application for analysis and synthesis problems with different types of dynamics and event-triggered implementations are provided.

ABSTRACT. We consider the problem of synthesizing symbolic output-feedback controllers which interact with a given plant via a pre-defined finite symbolic interface. We solve this problem by a new lazy abstraction-refinement technique which starts with a very coarse abstraction of the external trace semantics of the given plant and iteratively removes non-admissible behavior from this abstract model until a controller is found. We steer the search of controllers and abstract models towards small and concise state spaces representations by utilizing ideas from bounded synthesis. As a result, we obtain small and explainable controllers that are still powerful enough to solve the given synthesis problem. We have implemented our new synthesis method in the tool BOCoSy and show that BOCoSy is able to synthesize small, human readable symbolic controllers quickly on a set of benchmarks.

ABSTRACT. In this paper, we develop tools to analyze stability properties of discrete-time switched linear systems driven by switching signals belonging to a given omega - regular language. More precisely, we assume switching signals to be generated by a Buchi automaton where the alphabet corresponds to the modes of the switched system. We define notions of attractivity and uniform stability for this type of systems and also of uniform exponential stability when the considered Buchi automaton is deterministic. We then provide sufficient conditions to check these properties using Lyapunov and automata theoretic techniques. For a subclass of such systems with invertible matrices, we show that these conditions are also necessary. We finally show an example of application in the context of synchronization of oscillators over a communication network.

ABSTRACT. In the context of discrete-time switched systems, we investigate the comparison of stability certificates based on path-complete Lyapunov methods. A characterization of this general ordering has been provided recently, but we show here that this characterization is incomplete when a particular template is considered, as it is the case in practice. In the present work we provide a complete characterization for templates that are closed under pointwise minimum/maximum, which covers several templates that are often used in practice. We use an approach based on abstract operations on graphs, called lifts, to highlight the dependence of the ordering with respect to the analytical properties of the template. We finally provide more preliminary results on another family of templates: those that are closed under addition, as for instance the quadratic Lyapunov functions.

ABSTRACT. Switched systems are known to exhibit subtle (in)stability behaviors requiring system designers to carefully analyze the stability of closed-loop systems that arise from their proposed switching control laws. This paper presents a formal approach for verifying switched system stability that blends classical ideas from the controls and verification literature using differential dynamic logic (dL), a logic for deductive verification of hybrid systems. From controls, we use standard stability notions for various classes of switching mechanisms and their corresponding Lyapunov function-based analysis techniques. From verification, we use dL's ability to verify quantified properties of hybrid systems and dL models of switched systems as looping hybrid programs whose stability can be formally specified and proven by finding appropriate loop invariants, i.e., properties that are preserved across each loop iteration. This blend of ideas enables a trustworthy implementation of switched system stability verification in the KeYmaera X prover based on dL. For standard classes of switching mechanisms, the implementation provides fully automated stability proofs, including searching for suitable Lyapunov functions. Moreover, the generality of the deductive approach also enables verification of switching control laws that require non-standard stability arguments through the design of loop invariants that suitably express specific intuitions behind those control laws. This flexibility is demonstrated on three case studies: a model for longitudinal flight control by Branicky, an automatic cruise controller, and Brockett's nonholonomic integrator.