ABSTRACT. The falsification of a hybrid system aims at finding trajectories that violate a given safety property. This is a challenging problem, and the practical applicability of current falsification algorithms still suffers from their high time complexity. In contrast to falsification, verification algorithms aim at providing guarantees that no such trajectories exist. Recent symbolic reachability techniques are capable of efficiently computing linear constraints that enclose all trajectories of the system with reasonable precision. In this paper, we leverage the power of symbolic reachability algorithms to improve the scalability of falsification techniques. Recent approaches to falsification reduce the problem to a nonlinear optimization problem. We propose to reduce the search space of the optimization problem by adding linear state constraints obtained with a reachability algorithm. We showcase the efficiency of our approach on a number of standard hybrid systems benchmarks.

ABSTRACT. We investigate the information and guarantees provided by different inner and outer approximated reachability analyses, for proving properties of dynamical systems.We explore the connection of these approximated sets with the maximal and minimal reachable sets of Mitchell [33], with an additional notion of robustness to disturbance, as well as invariance and viability kernels. We demonstrate the practical use of a specific computation of these approximated reachable sets. We revisit in particular the reach-avoid properties. We also show how we can prove some new properties, such as every state of a given region is sure to be reached by the system, in presence of disturbances.

ABSTRACT. Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models that have inputs, nonlinear differential equations, and hybrid dynamics. As such, the scalability of affine systems verification is a prerequisite to the scalability of analysis methods for more complex systems. In this paper, we strive to improve the scalability of affine systems verification, in terms of the number of dimensions (variables) in the system.

One benefit of affine systems is that their reachable states can be written in terms of the matrix exponential, and safety checking can be performed at specific time steps with linear programming. Unfortunately, for large systems with many state variables, this direct approach requires an intractable amount of memory while using an intractable amount of computation time. We overcome these two problems by combining several methods that leverage common problem structure. Memory demands can be reduced by taking advantage of both initial states that are not full-dimensional, and safety properties (outputs) that only need a few linear projections of the state variables. Computation time is saved by using numerical simulations to compute only projections of the matrix exponential relevant for the verification problem. Since large systems often have sparse dynamics, we use fast Krylov-subspace simulation methods based on the Arnoldi or Lanczos iterations. Our implementation produces accurate counter-examples when properties are violated and, in the extreme case with sufficient problem structure, is shown to analyze a system with one billion real-valued state variables.

ABSTRACT. We present SReachTools, an open-source MATLAB toolbox for performing stochastic reachability of linear discrete-time systems that are perturbed by additive Gaussian noise. The toolbox addresses the problem of stochastic reachability of a target tube, which also encompasses the terminal-time hitting reach-avoid and viability problems. The stochastic reachability of a target tube problem maximizes the likelihood that the state of a stochastic system will remain within a time-varying target tube for a give time horizon, while respecting the system dynamics and bounded control authority. SReachTools implements several new algorithms, based on convex optimization, computational geometry, and on Fourier transforms, to efficiently compute over- and under-approximations of the stochastic reach set. SReachTools can be used to perform probabilistic verification of closed-loop systems, by providing probabilistic guarantees of safety and performance. In addition, SReachTools can also perform controller synthesis to assure probabilistic safety or performance, via open-loop or affine controllers. The code base is designed to be extensible and user friendly.

ABSTRACT. We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.

ABSTRACT. It is well known that (timed) ω-regular properties such as ‘p holds at every even position’ and ‘p occurs at least three times within the next 10 time units’ cannot be expressed in Metric Interval Temporal Logic (MITL) and Event Clock Logic (ECL). A standard remedy to this deficiency is to extend these with modalities defined in terms of automata. In this paper, we show that the logics EMITL0,∞ (adding non-deterministic finite automata modalities into the fragment of MITL with only lower- and upper-bound constraints) and EECL (adding automata modalities into ECL) are already as expressive as EMITL (full MITL with automata modalities). In particular, the satisfiability and model-checking problems for EMITL0,∞ and EECL are PSPACE-complete, whereas the same problems for EMITL are EXPSPACE-complete. We also provide a simple translation from EMITL0,∞ to diagonal-free timed automata, which enables practical satisfiability and model checking based on off-the-shelf tools.

ABSTRACT. Safety and security are major concerns in the development of Cyber-Physical Systems (CPS). Signal temporal logic (STL) was proposed as a language to specify and monitor the correctness of CPS relative to formalized requirements. Incorporating STL into a development process enables designers to automatically monitor and diagnose traces, compute robustness estimates based on requirements, and perform requirement falsification. These capabilities lead to potential high productivity gains in verification and validation activities; however, in its current form STL is agnostic to the input/output classification of signals, and this negatively impacts the relevance of the analysis results.

In this paper we propose to make the interface explicit in the STL language by introducing input/output signal declarations. We then define new measures of input vacuity and output robustness that better reflect the nature of the system and the specification intent. The resulting framework, which we call interface-aware signal temporal logic (IA-STL), aids verification and validation activities. We demonstrate the benefits of IA-STL on several CPS analysis activities: (1) robustness-driven sensitivity analysis, (2) falsification and (3) fault localization. We describe an implementation of our enhancement to STL and associated notions of robustness and vacuity in a prototype extension of Breach, a MATLAB/Simulink toolbox for CPS verification and validation. We explore these methodological improvements and evaluate our results on two examples from the automotive domain, an academic benchmark automatic transmission control model and an industrial hydrogen fuel cell system.

ABSTRACT. In multi-agent systems, robots transmit their planned trajectories to each other or to a central controller, and each receiver plans its own actions by maximizing a measure of mission satisfaction. For missions expressed in temporal logic, the \textit{robustness function} plays the role of satisfaction measure. Currently, a Piece-Wise Linear (PWL) or piece-wise constant fit is used at the receiver to reconstruct the continuous-time signal from the received samples. This allows an efficient robustness computation algorithm - a.k.a. \textit{monitoring} - but is not adaptive to the signal class of interest, and does not leverage the compression properties of more general representations. When communication capacity is at a premium, this is a serious bottleneck. In this paper we first show that the robustness computation is significantly affected by how the continuous-time signal is reconstructed from the received samples, which can mean the difference between a successful control and a crash. We show that monitoring general spline-based reconstructions yields a smaller robustness error, and that it can be done with in the same time complexity as monitoring the simpler PWL reconstructions. Thus robustness computation can now be adapted to the signal class of interest. We further show that the monitoring error is tightly upper-bounded by the $L_\infty$ signal reconstruction error. We present a (non-linear) $L_\infty$-based scheme which yields even lower monitoring error than the spline-based schemes (which have the advantage of being faster to compute), and illustrate all results on two case studies. As an application of these results, we show how time-frequency specifications can be efficiently monitored online.

ABSTRACT. We consider the decidability of state-to-state reachability in discrete- time linear time-invariant control systems, with control sets defined by boolean combinations of linear inequalities. It is a fundamental result in control theory that the version of this problem in which the control set is an affine subspace (i.e., definable by a conjunction of equations) is decidable in polynomial time.

We show that reachability is undecidable if the control set can be a finite union of affine subspaces. We moreover show that if the control set consists of a single affine subspace together with an additional point then reachability is as hard as Skolem's Problem for linear recurrence sequences. In like manner we show that if the control set in a convex polytope then reachability is as hard as the Positivity Problem for linear recurrence sequences.

Our main result shows decidability of the reachability problem for convex polytopic control sets under some spectral assumptions on the transition matrix of an LTI system.

ABSTRACT. Cyber-Physical Systems (CPSs) are integrations of distributed computing systems with physical processes via a networking with actuators and sensors, where the feedback loops among the components allow the physical processes to affect the computations and vice versa. Although CPSs can be found in several complex and sometimes critical real-world domains, their verification and validation often relies on simulation-test systems rather then formal methodologies. In this contribution, we prove the decidability of the reachability problem for a significant class of discrete-time linear CPSs whose physical process in isolation has a periodic behavior, up to a initial transitory phase.

ABSTRACT. Formal analysis of non-linear continuous and hybrid systems has recently attracted considerable attention. A common approach builds on computing a suitable finite discrete abstraction of the continuous system. In this paper, we propose a facetal abstraction which eliminates certain drawbacks of existing abstractions. The states of our abstraction are built primarily from facets of a polytopal partitioning of the system's state space taking thus into account the flow of the continuous dynamics and leading to global over-approximation. The transition system construction is based on queries solved by a delta-decision SMT-solver. The method is evaluated on several case studies.