We introduce PASTA (Perceptual Assessment System for explanaTion of Artificial Intelligence), a novel human-centric framework for evaluating eXplainable AI (XAI) techniques in computer vision. Our first contribution is the creation of the PASTA-dataset, the first large-scale benchmark that spans a diverse set of models and both saliency-based and concept-based explanation methods. This dataset enables robust, comparative analysis of XAI techniques based on human judgment. Our second contribution is an automated, data-driven benchmark that predicts human preferences using the PASTA-dataset. This scoring called PASTA-score method offers scalable, reliable, and consistent evaluation aligned with human perception. Additionally, our benchmark allows for comparisons between explanations across different modalities, an aspect previously unaddressed. We then propose to apply our scoring method to probe the interpretability of existing models and to build more human interpretable XAI methods.

Temporal Difference (TD) algorithms are widely used in Deep Reinforcement Learning (RL). Their performance is heavily influenced by the size of the neural network. While in supervised learning, the regime of over-parameterization and its benefits are well understood, the situation in RL is much less clear. In this paper, we present a theoretical analysis of the influence of network size and $l_2$-regularization on performance. We identify the ratio between the number of parameters and the number of visited states as a crucial factor and define over-parameterization as the regime when it is larger than one. Furthermore, we observe a double descent phenomenon, i.e., a sudden drop in performance around the parameter/state ratio of one. Leveraging random features and the lazy training regime, we study the regularized Least-Square Temporal Difference (LSTD) algorithm in an asymptotic regime, as both the number of parameters and states go to infinity, maintaining a constant ratio. We derive deterministic limits of both the empirical and the true Mean-Squared Bellman Error (MSBE) that feature correction terms responsible for the double descent. Correction terms vanish when the $l_2$-regularization is increased or the number of unvisited states goes to zero. Numerical experiments with synthetic and small real-world environments closely match the theoretical predictions.

Approximating the set of reachable states of a dynamical system is an algorithmic way to rigorously reason about its safety. Despite progress on efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in practice. While modern linear algebra packages are efficient for matrices with tens of thousands of dimensions, set-based image computations are limited to a few hundred. We propose to decompose reach-set computations such that set operations are performed in low dimensions, while matrix operations are performed in the full dimension. Our method is applicable in both dense- and discrete-time settings. For a set of standard benchmarks, we show a speed-up of up to two orders of magnitude compared to the respective state-of-the-art tools, with only modest loss in accuracy. For the dense-time case, we show an experiment with more than 10,000 variables, roughly two orders of magnitude higher than possible before.

Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.

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.

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 demonstrating the performance increase in speed and number of falsifyable instances.

Reachability analysis is difficult for hybrid automata with affine differential equations, because the reach set needs to be approximated. Promising abstraction techniques usually employ interval methods or template polyhedra. Interval methods account for dense time and guarantee soundness, and there are interval-based tools that overapproximate affine flowpipes. But interval methods impose bounded and rigid shapes, which make refinement expensive and fixpoint detection difficult. Template polyhedra, on the other hand, can be adapted flexibly and can be unbounded, but sound template refinement for unbounded reachability analysis has been implemented only for systems with piecewise constant dynamics. We capitalize on the advantages of both techniques, combining interval arithmetic and template polyhedra, using the former to abstract time and the latter to abstract space. During a CEGAR loop, whenever a spurious error trajectory is found, we compute additional space constraints and split time intervals, and use these space-time interpolants to eliminate the counterexample. Space-time interpolation offers a lazy, flexible framework for increasing precision while guaranteeing soundness, both for error avoidance and fixpoint detection. To the best of out knowledge, this is the first abstraction refinement scheme for the reachability analysis over unbounded and dense time of affine hybrid systems, which is both sound and automatic . We demonstrate the effectiveness of our algorithm with several benchmark examples, which cannot be handled by other tools.

Approximating the set of reachable states of a dynamical system is an algorithmic yet mathematically rigorous way to reason about its safety. Although progress has been made in the development of efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in the industrial setting. While modern linear algebra packages are efficient for matrices with tens of thousands of dimensions, set-based image computations are limited to a few hundred. We propose to decompose reach set computations such that set operations are performed in low dimensions, while matrix operations like exponentiation are carried out in the full dimension. Our method is applicable both in dense- and discrete-time settings. For a set of standard benchmarks, it shows a speed-up of up to two orders of magnitude compared to the respective state-of-the-art tools, with only modest losses in accuracy. For the dense-time case, we show an experiment with more than 10,000 variables, roughly two orders of magnitude higher than possible with previous approaches.

In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.

The tool Matlab/Simulink is a numerical simulation environment that is widely used in industry for model-based design. Numerical simulation scales well and can be applied to systems with highly complex dynamics, but it is also inherently incomplete in the sense that critical events or behavior may be overlooked. The application of formal verification techniques to Simulink models could help to overcome this limitation. Set-based verification tools such as SpaceEx use as underlying formalism hybrid automata, which are semantically and structurally different from Simulink models. To address this issue, we are building the tool SL2SX for transforming a subset of the Simulink modeling language into a corresponding SpaceEx model. Our method is designed to preserve the syntactic aspects of a given Simulink diagram: the resulting SpaceEx model shows the same hierarchical structure and preserves the names of components and variables. Placeholders with the correct interface are provided for unsupported Simulink blocks, which can then be translated manually. We illustrate the tool SL2SX and the verification of the transformed models in SpaceEx on two examples provided by the Mathworks example library.

We consider the problem of translating a deterministic \emph{simulation model} (like Matlab-Simunk, Modelica or Ptolemy models) into a \emph{verification model} expressed by a network of hybrid automata. The goal is to verify safety using reachability analysis on the verification model. Simulation models typically use transitions with urgent semantics, which must be taken as soon as possible. Urgent transitions also make it possible to decompose systems that would otherwise need to be modeled with a monolithic hybrid automaton.

Circuits and systems that have to deal with real valued artifacts often need to be evaluated not only for correct behaviors, but also the margins by which they satisfy the design intent. Our definition of "features" formally extends the classical notion of "assertions" by overlaying constructs for specifying real valued functions over matches of assertions, thereby providing a powerful language framework for specifying real valued properties of the system. In this paper we present, for the first time, methods for formal evaluation of feature ranges on hybrid automata models which are extensively used for modeling switched control systems. We demonstrate the methodology over three case studies, namely a cruise control system, a DC-DC Buck Regulator and a Li-ion battery charger.

Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space ). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error trajectory in the region space. A recent approach in this direction is based on guided search . Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, we propose an abstraction-based cost function based on coarse-grained space abstractions for guiding the reachability analysis. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.

In set-based reachability, a cover of the reachable states of a hybrid system is obtained by repeatedly computing one-step successor states. It can be used to show safety or to obtain quantitative information, e.g., for measuring the jitter in an oscillator circuit. In general, one-step successors can only be computed approximately and are difficult to scale in the number of continuous variables. The approximation error requires particular attention since it can accumulate rapidly, leading to a coarse cover, prohibitive state explosion, or preventing termination. In this paper, we propose an approach with precise control over the balance between approximation error and scalability. By lazy evaluation of set representations, the precision can be increased in a targeted manner, e.g., to show that a particular transition is spurious. Each evaluation step scales well in the number of continuous variables. The set representations are particularly suited for clustering and containment checking, which are essential for reducing the state explosion. This provides the building blocks for re ning the cover of the reachable set just enough to show a property of interest. The approach is illustrated on several examples.

Computing an approximation of the reachable states of a hybrid system is a challenge, mainly because overapproximating the solutions of ODEs with a finite number of sets does not scale well. Using template polyhedra can greatly reduce the computational complexity, since it replaces complex operations on sets with a small number of optimization problems. However, the use of templates may make the over-approximation too conservative. Spurious transitions, which are falsely considered reachable, are particularly detrimental to performance and accuracy, and may exacerbate the state explosion problem. In this paper, we examine how spurious transitions can be avoided with minimal computational effort. To this end, detecting spurious transitions is reduced to the well-known problem of showing that two convex sets are disjoint by finding a hyperplane that separates them. We generalize this to flowpipes by considering hyperplanes that evolve with time in correspondence to the dynamics of the system. The approach is implemented in the model checker SpaceEx and demonstrated on examples.

The theories underlying control engineering and real-time systems engineering use idealized models that mutually abstract from central aspects of the other discipline. Control theory usually assumes jitter-free sampling and negligible (constant) input-output latencies, disregarding complex real-world timing effects. Real-time systems theory uses abstract performance models that neglect the functional behavior and derives worst-case situations with limited expressiveness for control functions, e.g., In physically dominated automotive systems. In this paper, we propose an approach that integrates state-of-the art timing models into functional analysis. We combine physical, control and timing models by representing them as a network of hybrid automata. Closed-loop properties can then be verified on this hybrid automata network by using standard model checkers for hybrid systems. Since the computational complexity is critical for model checking, we discuss abstract models of timing behavior that seem particularly suited for this type of analysis. The approach facilitates systematic co-engineering between both control and real-time disciplines, increasing design efficiency and confidence in the system. The approach is illustrated by analyzing an industrial example, the control software of an electro-mechanical braking system, with the hybrid model checker Space Ex.

In this paper, we present an approximation of the set of reachable states, called flowpipe, for a continuous system with affine dynamics. Our approach is based on a representation we call flowpipe sampling, which consists of a set of continuous, interval-valued functions over time. A flowpipe sampling attributes to each time point a polyhedral enclosure of the set of states reachable at that time point, and is capable of representing a nonconvex enclosure of a nonconvex flowpipe. The use of flowpipe samplings allows us to represent and approximate the nonconvex flowpipe efficiently. In particular, we can measure the error incurred by the initial approximation and by further processing such as simplification and convexification. A flowpipe sampling can be efficiently translated into a set of convex polyhedra in a way that minimizes the number of convex sets for a given error bound. When applying flowpipe approximation for the reachability of hybrid systems, a reduction in the number of convex sets spawned by each image computation can lead to drastic performance improvements.

Properties of analog circuits can be verified formally by partitioning the continuous state space and applying hybrid system verification techniques to the resulting abstraction. To verify properties of oscillator circuits, cyclic invariants need to be computed. Methods based on forward reachability have proven to be inefficient and in some cases inadequate in constructing these invariant sets. In this paper, we propose a novel approach combining forward- and backward-reachability while iteratively refining partitions at each step. The technique can yield dramatic memory and runtime reductions. We illustrate the effectiveness by verifying, for the first time, the limit cycle oscillation behavior of a third-order model of a differential VCO circuit