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.

We propose an abstraction-refinement-based algorithm for the problem of verifying the safety of a camera-based autonomous system in a synthetic 3D-scene, based on the notion of interval images. An interval image is an abstract data structure that represents a set of images in a 3D-scene. We give a computer graphics style rendering algorithm to efficiently compute interval images from a given region. Our proposed abstraction-refinement algorithm leverages recent abstract interpretation tools for neural networks. We have implemented and evaluated the proposed technique on complex 3D-scenes, demonstrating its effectiveness and scalability in comparison with earlier techniques.

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.

In this paper, we study the probabilistic stability analysis of a subclass of stochastic hybrid systems, called the Planar Probabilistic Piecewise Constant Derivative Systems (Planar PPCD), where the continuous dynamics is deterministic, constant rate and planar, the discrete switching between the modes is probabilistic and happens at boundary of the invariant regions, and the continuous states are not reset during switching. These aptly model piecewise linear behaviors of planar robots. Our main result is an exact algorithm for deciding absolute and almost sure stability of Planar PPCD under some mild assumptions on mutual reachability between the states and the presence of non-zero probability self-loops. Our main idea is to reduce the stability problems on planar PPCD into corresponding problems on Discrete-time Markov Chains with edge weights. Our experimental results on PPCD benchmarks with various dynamics and number of modes, demonstrate the practical feasibility of this approach.

Coverage path planning (CPP) is the task of computing an optimal path within a region to completely scan or survey the area of interest by using robotic sensor footprints. In this work, we propose a novel approach to find the multi-robot optimal coverage path of an agricultural field using motion dynamics while minimizing the mission time. Our approach consists of three steps: (i) divide the agricultural field into convex polygonal areas to optimally distribute them among the robots, (ii) generate an optimal coverage path to ensure minimum coverage time for each of the polygonal areas, and (iii) generate the trajectory for each coverage path using Dubins motion dynamics. Several experiments and simulations were performed to check the validity and feasibility of our approach, and the results and limitations are discussed.

We consider the problem of verifying the safety of the trajectories of a camera-based autonomous vehicle in a given 3-D-scene. We give a procedure to verify that all trajectories starting from a given initial region reach a specified target region safely without colliding with obstacles on the way. We also give a prioritization-based falsification procedure that collects unsafe trajectories. Both our procedures are based on the key notion of image-invariant regions, which are regions within which the captured images are identical. We evaluate our methods on a model of an autonomous road-following drone in a variety of 3-D-scenes; our experimental results demonstrate the feasibility and benefits of our approach for both safety analysis and falsification.

Abstract In this paper, we investigate the design of a safe hybrid controller for an aircraft that switches between a classical linear quadratic regulator (LQR) controller and a more intelligent artificial neural network (ANN) controller. Our objective is to switch safely between the controllers, such that the aircraft is always recoverable within a fixed amount of time while allowing the maximum time of operation for the ANN controller. There is a priori known safety zone for the LQR controller operation in which the aircraft never stalls, over accelerates, or exceeds maximum structural loading, and hence, by switching to the LQR controller just before exiting this zone, one can guarantee safety. However, this priori known safety zone is conservative, and therefore, limits the time of operation for the ANN controller. We apply reachability analysis to expand the known safety zone, such that the LQR controller will always be able to drive the aircraft back to the safe zone from the expanded zone (“recoverable zone") within a fixed duration. The “recoverable zone" extends the time of operation of the ANN controller. We perform simulations using the hybrid controller corresponding to the recoverable zone and observe that the design is indeed safe.

In this paper, we investigate the problem of generating time-optimal trajectories automatically for spraying pesticides to infected regions with varying degree of infections in an agricultural field using a collection of quad-rotors that have limited pesticide carrying capacity but are capable of refilling from the pesticide tanks stationed across the field. We consider the time of traversal between points, time for changing the direction of traversal, and time for spraying and refilling, explicitly in the problem formulation, and generate trajectories for the multiple quad-rotors to execute in parallel such that the total energy (time) for completion of the task is minimized. We present two methods namely, multiple traveling salesman based time-optimal trajectory generation, and clustering based de-compositional time-optimal trajectory generation, respectively. In the first method, our approach consists of reducing the time-optimal trajectory generation problem for the multiple quad-rotors to a version of the multiple traveling salesman problem on a weighted graph, and then encoding the problem into a mixed integer linear programming problem. In the second method, our approach consists of first decomposing the infected regions into k clusters corresponding to the k robots, placing each quad-rotor at the center of the corresponding clusters, and finally, independently solving time-optimal trajectory generation problem for each quad-rotor using the first method. We have implemented both the approaches and performed experimental comparison. We observe that the first method provides an optimal strategy, while the second method provides a sub-optimal strategy. However, the second method is computationally more efficient, and the loss of optimality is minimal, hence, it provides a better trade-off between the computational complexity and the optimality constraints.

We study the problem of safety verification of linear discrete-time stochastic systems (linear DTSS) over bounded and unbounded time horizons. Linear DTSS capture random processes, where the one-step transition relation between the current random vector X and the next-step random vector X' is linear and is given by X' = AX + W, where A is an n × n matrix and W is a random noise vector. We assume that the initial and noise random vectors are multivariate normal. Our safety problem consists of checking whether a random vector in the unsafe set is reachable from a random vector in the initial set through a random process of the linear DTSS in either a given bounded or unbounded number of steps. For bounded safety verification, we reduce the problem to the satisfiability of a semidefinite programming problem. For the unbounded safety verification, we propose a novel abstraction procedure to reduce the safety problem to that of a finite graph, wherein, the nodes of the graph correspond to the regions of a partition of the random vector space, in contrast to existing works that partition the state-space. More precisely, we partition the parameter space of normal random vectors, namely, the space of means and covariance matrices, and apply semi-definite programming to compute the edges. We show that our abstraction procedure is sound.

In this paper, we propose a Bayesian approach to statistical model-checking (SMC) of discrete-time Markov chains with respect to continuous stochastic logic (CSL) specifications. While Bayesian approaches for simpler logic without nested probabilistic operators and Frequentist approaches for nested logic have been previously explored, the Bayesian approach for CSL consisting of nested probabilistic operators has not been addressed. The challenge in the nested case arises from the fact that unlike in probabilistic model-checking (PMC), where we obtain a definitive answer for the model-checking problem for the sub-formulas, instead, we only obtain a correct answer with a certain confidence, which needs to be factored into the recursive SMC algorithm. Here, we propose a Bayesian test based algorithm for CSL that has nested probabilistic operators. We have implemented our algorithm in a Python Toolbox. Our experimental evaluation shows that our Bayesian SMC approach performs better than both the frequentist SMC approach and PMC algorithms.

We propose a novel hybridization method for stability analysis that over-approximates nonlinear dynamical systems by switched systems with linear inclusion dynamics. We observe that existing hybridization techniques for safety analysis that over-approximate nonlinear dynamical systems by switched affine inclusion dynamics and provide fixed approximation error, do not suffice for stability analysis. Hence, we propose a hybridization method that provides a state-dependent error which converges to zero as the state tends to the equilibrium point. The crux of our hybridization computation is an elegant recursive algorithm that uses partial derivatives of a given function to obtain upper and lower bound matrices for the over-approximating linear inclusion. We illustrate our method on some examples to demonstrate the application of the theory for stability analysis. In particular, our method is able to establish stability of a nonlinear system which does not admit a polynomial Lyapunov function.

We consider the problem of bounded time safety verification of interconnections of input-output continuous dynamical systems. We present a compositional framework for computing bounded error approximations of the complete system from those of the components. The main crux of our approach consists of capturing the input-output signal behaviors of a component using an abstraction predicate that represents the input-output sample behaviors corresponding to the signal behaviors. We define a semantics for the abstraction predicate that captures an over-approximation of the input-output signal behaviors of a component. Next, we define how to compose abstraction predicates of components to obtain an abstraction predicate for the composed system. We instantiate our compositional abstraction construction framework for linear dynamical systems by providing concrete methods for constructing the input-output abstraction predicates for the individual systems.

In this paper, we consider the problem of output range analysis for feed-forward neural networks. The current approaches reduce the problem to satisfiability and optimization solving which are NP-hard problems, and whose computational complexity increases with the number of neurons in the network. We present a novel abstraction technique that constructs a simpler neural network with fewer neurons, albeit with interval weights called interval neural network (INN) which over-approximates the output range of the given neural network. We reduce the output range analysis on the INNs to solving a mixed integer linear programming problem. Our experimental results highlight the trade-off between the computation time and the precision of the computed output range.

We consider the problem of safety analysis of probabilistic hybrid systems, which capture discrete, continuous and probabilistic behaviors. We present a novel counterexample guided abstraction refinement (CEGAR) algorithm for a subclass of probabilistic hybrid systems, called polyhedral probabilistic hybrid systems (PHS), where the continuous dynamics is specified using a polyhedral set within which the derivatives of the continuous executions lie. Developing a CEGAR algorithm for PHS is complex owing to the branching behavior due to the probabilistic transitions, and the infinite state space due to the real-valued variables. We present a practical algorithm by choosing a succinct representation for counterexamples, an efficient validation algorithm and a constructive method for refinement that ensures progress towards the elimination of a spurious abstract counterexample. The technical details for refinement are non-trivial since there are no clear disjoint sets for separation. We have implemented our algorithm in a Python toolbox called Procegar; our experimental analysis demonstrates the benefits of our method in terms of successful verification results, as well as bug finding.

We investigate how the semantics of a hybrid automaton deviates with respect to syntactic perturbations on the hybrid automaton. We consider syntactic perturbations of a hybrid automaton, wherein the syntactic representations of its elements, namely, initial sets, invariants, guards, and flows, in some logic are perturbed. Our main result establishes a continuity like property that states that small perturbations in the syntax lead to small perturbations in the semantics. More precisely, we show that for every real number epsilon>0 and natural number k, there is a real number delta>0 such that H^delta, the delta syntactic perturbation of a hybrid automaton H, is epsilon-simulation equivalent to H up to k transition steps. As a byproduct, we obtain a proof that a bounded safety verification tool such as dReach will eventually prove the safety of a safe hybrid automaton design (when only non-strict inequalities are used in all constraints) if dReach iteratively reduces the syntactic parameter delta that is used in checking approximate satisfiability. This has an immediate application in counter-example validation in a CEGAR framework, namely, when a counter-example is spurious, then we have a complete procedure for deducing the same.

In this paper, we explain the architecture and implementation of the tool Averist that performs stability verification for linear hybrid systems. This tool implements a hybridization method for approximating linear hybrid systems by hybrid systems with polyhedral inclusion dynamics. It also implements a new counterexample guided abstraction refinement framework for analyzing the hybrid systems with polyhedral inclusion dynamics that are generated as a result of the hybridization. Some of the main features of our tool are as follows: (1) our tool is based on algorithmic techniques that do not rely on the computation of Lyapunov functions, (2) it returns a counterexample when it fails to establish stability, (3) it is less prone to numerical instability issues as compared to Lyapunov function based tools.

In this work, we present a novel technique to automatically generate satisfying and violating traces for a Signal Temporal Logic (STL) formula. STL is a logic whose formulas are interpreted over real-valued signals that evolve over dense time, which is a natural setting for Cyber-Physical Systems (CPS) applications. However, the process of developing appropriate STL requirements can be difficult and error prone. In this work, we provide a method to assist designers in the development of STL requirements for CPS applications. Our technique automatically encodes a given STL formula into a satisfiability modulo theory (SMT) formula in an appropriate theory. Satisfying and violating traces for the STL specification can be obtained by solving satisfiability problems on the encoded SMT formulas. In particular, models returned by the SMT solver correspond to traces that satisfy/violate the STL formula, thus offering a window into the types of behaviors specified by the formula. We demonstrate how the method can be used to debug problems with STL requirements, and we evaluate the performance of the method on a collection of requirements developed for CPS applications.

In this paper, we describe an abstraction-based method for synthesizing a state-based switching control for stabilizing a family of dynamical systems. Given a set of dynamical systems and a set of polyhedral switching surfaces, the algorithm synthesizes a strategy that assigns to every surface the linear dynamics to switch to at the surface. Our algorithm constructs a finite game graph that consists of the switching surfaces as the existential nodes and the choices of the dynamics as the universal nodes. In addition, the edges capture quantitative information about the evolution of the distance of the state from the equilibrium point along the executions. A switching strategy for the family of dynamical systems is extracted by finding a strategy on the game graph which results in plays having a bounded weight. Such a strategy is obtained by reducing the problem to the strategy synthesis for an energy game, which is a well-studied problem in the literature. We have implemented our algorithm for polyhedral inclusion dynamics and linear dynamics. We illustrate our algorithm on examples from these two classes of systems.

Timed automata have an idealized semantics where clocks are assumed to be perfectly continuous and synchronized, and guards have infinite precision. These assumptions cannot be realized physically. In order to ensure that correct timed automata designs can be implemented on real-time platforms, several authors have suggested that timed automata be stud- ied under robust semantics. A timed automaton H is said to robustly satisfy a property if there is a positive -- and/or a positive -- such that the automaton satisfies the property even when the clocks are allowed to drift by epsilon and/or guards are enlarged by delta. In this paper we show that, 1. checking omega-regular properties when only clocks are perturbed or when both clocks and guards are perturbed, is PSPACE-complete; and 2. one can compute the exact reachable set of a bounded timed automaton when clocks are drifted by infinitesimally small amount, using polynomial space. In particular, we re- move the restrictive assumption on the timed automaton that its region graph only contains progress cycles, under which the second result above has been previously established.

In this paper, we present an algorithmic approach to global asymptotic stability (GAS) verification of hybrid systems. Our broad approach consists of reducing the GAS verification to the verification of a region stability (RS) analysis problem and an asymptotic stability (AS) analysis problem. We use a recently developed quantitative predicate abstraction technique for AS analysis and extract from it a stability zone with respect to which we perform RS analysis. We present a new algorithm for RS analysis based on abstractions. While we develop the theory for polyhedral hybrid systems, our broad approach of decomposing GAS analysis to RS and AS analysis can be applied to more general class of systems including linear hybrid systems. As a proof of concept, we apply the GAS verification algorithm to a linear hybrid system model of a cruise control for an automatic gearbox, and provide a semi-automated proof of GAS.

In this paper, we present a hybridization method for stability analysis of switched linear hybrid system (LHS), that constructs a switched system with polyhedral inclusion dynamics (PHS) using a state-space partition that is specific to stability analysis. We use a previous result based on quantitative predicate abstraction to analyse the stability of PHS. We show completeness of the hybridization based verification technique for the class of asymptotically stable linear system and a subclass of switched linear systems whose dynamics are pairwise Lipschitz continuous on the state-space and uniformly converging in time. For this class of systems, we show that by increasing the granularity of the region partition, we eventually reach an abstract switched system with polyhedral inclusion dynamics that is asymptotically stable. On the practical side, we implemented our approach in the tool averist, and experimentally compared our approach with a state-of-the-art tool for stability analysis of hybrid systems based on Lyapunov functions. Our experimental results illustrate that our method is less prone to numerical errors and scales better than the traditional approaches. In addition, our tool returns a counterexample in the event that it fails to prove stability, providing feedback regarding the potential reason for instability. We also examined heuristics for the choice of state-space partition during refinement.

We consider the problem of computing a bounded error approximation of the solution over a bounded time [0,T], of a parameterized linear system, x(t) = Ax(t), where A is constrained by a compact polyhedron Ω. Our method consists of sampling the time domain [0,T] as well as the parameter space Ω and constructing a continuous piecewise bilinear function which interpolates the solution of the parameterized system at these sample points. More precisely, given an ε > 0, we compute a sampling interval δ > 0, such that the piecewise bilinear function obtained from the sample points is within ε of the original trajectory. We present experimental results which suggest that our method is scalable.

We investigate the problem of verifying the absence of zeno executions in a hybrid system. A zeno execution is one in which there are infinitely many discrete transitions in a finite time interval. The presence of zeno executions poses challenges towards implementation and analysis of hybrid control systems. We present a simple transformation of the hybrid system which reduces the non-zenoness verification problem to the termination verification problem, that is, the original system has no zeno executions if and only if the transformed system has no non-terminating executions. This provides both theoretical insights and practical techniques for non-zenoness verification. Further, it also provides techniques for isolating parts of the hybrid system and its initial states which do not exhibit zeno executions. We illustrate the feasibility of our approach by applying it on hybrid system examples.

Motivated by designing high-level planners for dynamical systems (such as mobile robots) to achieve complex tasks, we consider the synthesis of switching controllers of nonlinear dynamical systems from metric temporal logic (MTL) specifications. MTL is a popular logic that allows to specify timed properties of real-time reactive systems and hence is appropriate for describing the safe and autonomous operations of robotic systems in an uncertain and possibly adversarial environment. We provide constructive means for computing finite-state abstractions that preserve MTL properties for nonlinear systems, under a weak assumption that these nonlinear systems evolve continuously with respect to their initial conditions. We then provide conditions to ensure that the existence of a discrete strategy (obtained by solving a discrete synthesis problem) guarantees the existence of a switching strategy for controlling the continuous-time dynamical systems to satisfy a given MTL specification. We illustrate the results on a motion planning problem.

Pre-orders on systems are the basis for abstraction based verification of systems. In this paper, we investigate pre-orders for reasoning about stability with respect to inputs of hybrid systems. First, we present a superposition type theorem which gives a characterization of the classical incremental input-to-state stability of continuous systems in terms of the traditional ε-δ definition of stability. We use this as the basis for defining a notion of incremental input-to-state stability of hybrid systems. Next, we present a pre-order on hybrid systems which preserves incremental input-to-state stability, by extending the classical definitions of bisimulation relations on systems with input, with uniform continuity constraints. We show that the uniform continuity is a necessary requirement by exhibiting counter-examples to show that weaker notions of input bisimulation with just continuity requirements do not suffice to preserve stability. Finally, we demonstrate that the definitions are useful, by exhibiting concrete abstraction functions which satisfy the definitions of pre-orders.

A rectangular switched hybrid system with polyhedral invariants and guards, is a hybrid automaton in which every continuous variable is constrained to have rectangular flows in each control mode, all invariants and guards are described by convex polyhedral sets, and the continuous variables are not reset during mode changes. We investigate the problem of checking if a given rectangular switched hybrid system is stable around the equilibrium point 0. We consider both Lyapunov stability and asymptotic stability. We show that checking (both Lyapunov and asymptotic) stability of planar rectangular switched hybrid systems is decidable, where by planar we mean hybrid systems with at most 2 continuous variables. We show that the stability problem is undecidable for systems in 5 dimensions, i.e., with 5 continuous variables.

We present a method for mending strategies for GR(1) specifications. Given the addition or removal of edges from the game graph describing a problem (essentially transition rules in a GR(1) specification), we apply a μ-calculus formula to a neighborhood of states to obtain a “local strategy” that navigates around the invalidated parts of an original synthesized strategy. Our method may thus avoid global resynthesis while recovering correctness with respect to the new specification. We illustrate the results both in simulation and on physical hardware for a planar robot surveillance task.

Pre-orders between processes, like simulation, have played a central role in the verification and analysis of discrete-state systems. Logical characterization of such pre-orders have allowed one to verify the correctness of a system by analyzing an abstraction of the system. In this paper, we investigate whether this approach can be feasibly applied to reason about stability properties of a system.

In this paper we consider the problem of approximating the set of states reachable within a time bound T in a linear dynamical system, to within a given error bound ε. Fixing a degree d, our algorithm divides the interval [0,T] into sub-intervals of not necessarily equal size, such that a polynomial of degree d approximates the actual flow to within an error bound of ε, and approximates the reach set within each sub-interval by the polynomial tube. Our experimental evaluation of the algorithm when the degree d is fixed to be either 1 or 2, shows that the approach is promising, as it scales to large dimensional dynamical systems, and performs better than previous approaches that divided the interval [0,T] evenly into sub-intervals.

In this paper, we approximate a hybrid system with arbitrary flow functions by systems with polynomial flows; the verification of certain properties in systems with polynomial flows can be reduced to the first order theory of reals, and is therefore decidable. The polynomial approximations that we construct ¿-simulate (as opposed to "simulate'') the original system, and at the same time are tight. We show that for systems that we call tolerant, safety verification of a system can be reduced to the safety verification of the polynomial approximation. Our main technical tool in proving this result is a logical characterization of ¿-simulations. We demonstrate the construction of the polynomial approximation, as well as the verification process, by applying it to an example protocol in air traffic coordination.

This paper presents general techniques for formally modeling, simulating, and model checking real-time resource-sharing protocols in Real-Time Maude. The "scheduling subset" of our techniques has been used to find a previously unknown subtle bug in a state-of-the-art scheduling algorithm. This paper also shows how our general techniques can be instantiated to model and analyze the well known priority inheritance protocol.