CPSWEEK

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

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

Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models with inputs, nonlinear differential equations, and hybrid dynamics. As such, the scalability of affine systems ...

We present SReachTools, an open-source MATLAB toolbox for performing stochastic reachability of linear, potentially time-varying, discrete-time systems that are perturbed by a stochastic disturbance. The toolbox addresses the problem of stochastic ...

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

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

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

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

We consider the decidability of state-to-state reachability in linear time-invariant control systems over discrete time. We analyse this problem with respect to the allowable control sets, which in general are assumed to be defined by boolean ...

Cyber-Physical Systems (CPSs) are integrations of distributed computing systems with physical processes via a networking with actuators and sensors, where feedback loops among the components allow the physical processes to affect the computations and ...

Formal analysis of non-linear continuous and hybrid systems is a hot topic. 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 ...

This paper investigates characterizations of safety in terms of barrier functions for hybrid systems modeled by hybrid inclusions. After introducing an adequate definition of safety for hybrid inclusions, sufficient conditions using continuously ...

This paper studies topological entropy and stability properties of switched linear systems. First, we show that the exponential growth rates of solutions of a switched linear system are essentially upper bounded by its topological entropy. Second, we ...

In this paper we study the problem of computing robust invariant sets for state-constrained perturbed polynomial systems within the Hamilton-Jacobi reachability framework. A robust invariant set is a set of states such that every possible trajectory ...

We study criteria allowing to compare the conservativeness of stability certificates for switching systems. The stability certificates under consideration are Path-Complete Lyapunov functions (PCLFs), which are multiple Lyapunov functions with an ...

In this paper, we consider the problem of formally verifying the safety of an autonomous robot equipped with a Neural Network (NN) controller that processes LiDAR images to produce control actions. Given a workspace that is characterized by a set of ...

We present an approach to construct reachable set overapproximations for continuous-time dynamical systems controlled using neural network feedback systems. Feedforward deep neural networks are now widely used as a means for learning control laws ...

This paper presents Verisig, a hybrid system approach to verifying safety properties of closed-loop systems using neural networks as controllers. We focus on sigmoid-based networks and exploit the fact that the sigmoid is the solution to a quadratic ...

Neural Networks (NN) have been proposed in the past as an effective means for both modeling and control of systems with very complex dynamics. However, despite the extensive research, NN-based controllers have not been adopted by the industry for safety ...

We consider the problem of extracting safe environments and controllers for reach-avoid objectives for systems with known state and control spaces, but unknown dynamics. In a given environment, a common approach is to synthesize a controller from an ...

Weakly-hard systems are real-time systems that can tolerate occasional deadline misses in a bounded manner. Compared with traditional systems with hard deadline constraints, they provide more scheduling flexibility, and thus expand the design space for ...

In the first part of this paper, we solve the problem of verifying stability of an interconnection of embedded control systems under a timing contract which specifies the time instants at which some operations in each subsystem are performed such as ...

Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic (LTL) specifications. Technically, robustness was formalized in the logic rLTL via 5 different truth values and it led to an increase ...

This paper presents TIRA, a Matlab library gathering several methods for the computation of interval over-approximations of the reachable sets for both continuous- and discrete-time nonlinear systems. Unlike other existing tools, the main strength of ...

In this paper we study how to formulate the optimal control problem for a piecewise-affine dynamical system as a mixed-integer program. Problems of this form arise typically in hybrid Model Predictive Control (MPC), where at every time step an open-loop ...

This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications over both finite- and ...

The correctness of control software in many safety-critical applications such as autonomous vehicles is crucial. One technique to achieve correct control software is called "symbolic control", where complex systems are approximated by finite-state ...

Stochastic hybrid systems (SHS) are a rich mathematical modelling framework capable of describing complex systems, where uncertainty and hybrid (that is, both continuous and discrete) components are relevant. We introduce a new software tool - StocHy-...

Hyperbolicity is a cornerstone of nonlinear systems theory. Hyperbolic dynamics are characterized by the presence of expanding and contracting directions for the derivative along the trajectories of the system. Hyperbolic dynamical systems enjoy many ...

We present an approach for the synthesis and verification of neural network controllers for closed loop dynamical systems, modelled as an ordinary differential equation. Feedforward neural networks are ubiquitous when it comes to approximating functions,...