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 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.

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.

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.

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.