In this article, we consider the problem of reachable set computation of a closed-loop system with anytime sensor and a neural network controller. We provide a star set data structure-based forward propagation algorithm that uses existing efficient operations on star-sets and a novel convex hull construction. We present rigorous analysis of the space-complexity of the star sets generated during the propagation. Our experimental results show significant improvement with respect to existing methods that use vertex-based representation of polyhedral sets for propagation through closed-loop systems with anytime sensing, as well as the feasibility of the approach on different types of dynamics, control and sensors.

In this paper, we consider the problem of safety analysis of a closed-loop control system with anytime perception sensor. We formalize the framework and present a general procedure for safety analysis using reachable set computation. We instantiate the procedure for two concrete classes, namely, the classical discrete-time linear system with linear state feedback controller and an extension with variable update rates. We present an exact computational method based on polyhedral manipulations for the first class and an overapproximate method for the second class. Our experimental results demonstrate the feasibility of the approach.

In this article, we consider the problem of checking approximate conformance of closed-loop systems with the same plant but different neural network (NN) controllers. First, we introduce a notion of approximate conformance on NNs, which allows us to quantify semantically the deviations in closed-loop system behaviors with different NN controllers. Next, we consider the problem of computationally checking this notion of approximate conformance on two NNs. We reduce this problem to that of reachability analysis on a combined NN, thereby, enabling the use of existing NN verification tools for conformance checking. Our experimental results on an autonomous rocket landing system demonstrate the feasibility of checking approximate conformance on different NNs trained for the same dynamics, as well as the practical semantic closeness exhibited by the corresponding closed-loop systems.