Pour le prochain séminaire de l’équipe Cosynus, nous aurons le plaisir d’accueillir Goran Frehse et Mirco Giacobbe qui nous parleront d’atteignabilité. Les deux exposés se suivent et devraient durer 30 minutes chacun.

Goran Frehse – Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices

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

Goran Frehse received a Diploma in electrical engineering and information technology from Karlsruhe Institute of Technology and a PhD in computer science from Radboud University Nijmegen. From 2006 to 2018, he was an associate professor at the University Grenoble Alpes, holding a research fellowship (chaire) from 2016. Since 2018, he is an associate professor at ENSTA ParisTech. He is the architect and lead developer of two well-known model checking tools for hybrid and cyber-physical systems, PHAVer and SpaceEx.

Mirco Giacobbe – Refining Template-polyhedra from Counterexamples

Abstract: Template polyhedra generalize intervals and octagons to polyhedra whose facets are normal to arbitrary sets of directions. They are successfully employed by SpaceEx in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user, this talk presents a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. The method applies to linear and nonlinear hybrid automata with constant derivatives, and to hybrid automata with linear ODE. Our experiments demonstrate its efficacy on the time-unbounded reachability of several benchmarks.

Mirco Giacobbe received BSc and MSc from the University of Trento and MSc from RWTH AAchen, in computer Science. Today he is a PhD student in Henziger’s group, at IST Austria. His work focuses on the analysis of timed and hybrid systems and on the application of formal methods in artificial intelligence and systems biology.