ABSTRACT. Ensuring the trust and safety of autonomous systems demands an expansion of formal methodologies to accommodate a broader array of models and assumptions. In the first part of this talk, I will discuss methods of assessing system safety through reachability analysis and how different model assumptions impact their effectiveness. These methods combine simulation data with sensitivity analysis for answering questions about system safety. At one end, complete dynamical models offer strong assurances, but their utility can be limited. Allowing probabilistic notions of sensitivity, we get algorithms capable of addressing real-world scenarios. This flexible approach informs our current work on the Verse framework which aims to make code-level analysis for autonomous multi-agent scenarios accessible to undergraduates. In the second part, I will discuss a safety analysis method for learning-enabled autonomous systems using abstraction and substitutivity. Specifically, this derives the conditions when a hypothetical ideal observer can be substituted with a practical observer implemented by a machine learning model. This leads to the notion of a perception contract which approximates the machine learning model and it can substitute a perfect observer while preserving the safety proof. We will discuss applications of this method in the analysis for vision-based lane keeping and automated landing systems.

ABSTRACT. We propose an approach to compute inner and outer-approximations of the sets of values satisfying constraints expressed as arbitrarily quantified formulas. Such formulas arise for instance when specifying important problems in control such as robustness, motion planning or controllers comparison. We propose an interval-based method which allows for tractable but tight approximations. We demonstrate its applicability through a series of examples and benchmarks using a prototype implementation.

ABSTRACT. This paper presents temporal behavior trees (TBT), a specification formalism inspired by behavior trees that are commonly used to program robotic applications. We then introduce the concept of trace segmentation, wherein given a TBT specification and a trace, we split the trace optimally into sub-traces that are associated with various portions of the TBT specification. Segmentation of a trace then serves to explain precisely how a trace satisfies/violates a specification, and which portions of a specification are actually violated. We introduce the syntax and semantics of TBT and compare their expressiveness in relation to temporal logic. We also show that the use of behavior tree operators makes the specifications easy to express in many cases. Next, we define robustness semantics for TBT specification with respect to a trace. Rather than a true/false interpretation, the robustness provides a real-valued numerical outcome that quantifies how close or far away a trace is from satisfying/violating a TBT specification. We show that computing the robustness of a trace also segments it into subtraces associated with parts of the behavior tree specification. Finally, we provide efficient approximations for computing robustness and segmentation for long traces with guarantees on the resulting approximate answer. We demonstrate how segmentations are useful through applications such as understanding how novice users pilot a aerial vehicle through a sequence of waypoints in desktop experiments and the offline monitoring of automated lander for a drone on a ship in the presence of powerful disturbances. Our case studies demonstrate how TBT specification and segmentation can be used to understand and interpret complex behaviors of humans and automation in cyber-physical systems.

ABSTRACT. A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures---such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT)---barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute LTL and $\omega$-regular specifications by separating consecutive transitions of corresponding $\omega$-automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We augment these definitions with SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness over some case studies.

ABSTRACT. We consider the problem of computing distributed logical controllers for two interacting system components via a novel sound and complete contract-based synthesis framework. Based on a discrete abstraction of component interactions as a two-player game over a finite graph and specifications for both components given as $\omega$-regular (e.g. LTL) properties over this graph, we co-synthesize contract and controller candidates locally for each component and propose a negotiation mechanism which iteratively refines these candidates until a solution to the given distributed synthesis problem is found. Our framework relies on the recently introduced concept of permissive templates which collect an infinite number of controller candidates in a concise data structure. We utilize the efficient computability, adaptability and compositionality of such templates to obtain an efficient, yet sound and complete negotiation framework for contract-based distributed logical control. We showcase the superior performance of our approach by comparing our prototype tool CoSMo to state-of-the-art tools on a robot motion planning benchmark suite.

ABSTRACT. We present an abstract interpretation approach for synthesizing nonlinear (semi-algebraic) positive invariants for systems of polynomial ordinary differential equations (ODEs) and switched systems. The key behind our approach is to connect the system under study to a positive nonlinear system through a ``change of variables''. The positive invariance of the first orthant ($\Re_+$ ) for a positive system guarantees, in turn, that the functions involved in the change of variables define a positive invariant for the original system. The challenge lies in discovering such functions for a given system. To this end, we characterize positive invariants as fixed points under an operator that is defined using the Lie derivative. Next, we use abstract interpretation approaches to systematically compute this fixed point. Whereas abstract interpretation has been applied to the static analysis of programs, and invariant synthesis for hybrid systems to a limited extent, we show how these approaches can compute fixed points over cones generated by polynomials using sum-of-squares optimization and its relaxations. Our approach is shown to be promising over a set of small but hard-to-analyze nonlinear models, wherein it is able to generate positive invariants to place useful bounds on their reachable sets.

ABSTRACT. Formal synthesis of safe controllers is essential for safety-critical cyber-physical systems. In this paper, we propose a novel counterexample guided approach for synthesizing safe controllers of nonlinear systems using Bayesian optimization enhanced reinforcement learning, to improve the efficiency of the training process while ensuring safety property. First, we utilize the control barrier function technique to establish a constrained Markov decision process, which enables us to learn an initial controller with minimal safety violations. We then design a counterexample-guided policy refinement using Bayesian optimization, to fine-tune the initial controller based on the failure trajectories. Finally, we design a compensatory controller by an adaptive mechanism to refine the tuned controller to guarantee the safety. We implement the $CEGRLPR$ tool and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our approach.

ABSTRACT. We introduce the concept of memoryless concretization relation (MCR) to describe abstraction within the context of controller synthesis. This relation is a specific instance of alternating simulation relation (ASR), where it is possible to simplify the controller architecture. In the case of ASR, the concretized controller needs to simulate the concurrent evolution of two systems, the original and abstract systems, while for MCR, the designed controllers only need knowledge of the current concrete state. We demonstrate that the distinction between ASR and MCR becomes significant only when a non-deterministic quantizer is involved, such as in cases where the state space discretization consists of overlapping cells. We also show that any abstraction of a system that alternatingly simulates a system can be completed to satisfy MCR at the expense of increasing the non-determinism in the abstraction. We clarify the difference between the MCR and the feedback refinement relation (FRR), showing in particular that the former allows for non-constant controllers within cells. This provides greater flexibility in constructing a practical abstraction, for instance, by reducing non-determinism in the abstraction. Finally, we prove that this relation is not only sufficient, but also necessary, for ensuring the above properties.