Overview

Methods from fundamental computer science have been pervasive to many scientific and technological domains. In particular, the combination between formal methods and control theory has proven very fruitful since the 1990s, with hybrid automata and hybrid systems theory, the use of variants and invariants (Lyapunov functions in control theory), reachability methods etc.

More recently, the second advent of artificial intelligence has fostered once again new fruitful interactions with formal methods during the five last years, in particular when neural networks are used in place of more classical controllers (e.g. obtained as optimal controllers of some sort, using reinforcement learning) or used as sensors, for perception, within the feedback control loop.

In control, where continuous mathematics plays a big role, the geometry of the state space and of the set of possible (controlled) trajectories is naturally considered, for all application purposes. Proto-geometric methods already paves the way: reachability methods, that are generally using set-based methods, i.e. abstract interpretation domains (polyhedra, zonotopes, ellipsoids etc.) synthesize guaranteed outer-approximations of sets of reachables states or of tubes of trajectories. Getting or using finer knowledge about these sets buys you more, and in particular computability (including in some cases, actual algorithms) and complexity of control, or robotic tasks. This is even more so when considering distributed control tasks, bridging the gap with geometry as developed in e.g. fault-tolerant distributed computing.

Course objective

The objective of the course is to present the students with recent semantic abstractions for (possibly distributed) controlled and AI-based systems. These are further exploited in several directions: computability, complexity and verification.

These semantic abstractions are all based on recent abstract interpretation methods for guaranteed inner and outer approximation of subsets of R^n, and of subsets of numerical functions from R^m to R^n. The geometric (e.g. algebraic topological invariants) extracted from these inner and outer approximations give finer information exploited for invariant synthesis, computability results and complexity characterizations.

Prerequisites

Basic knowledge of bachelor level mathematics and computer science (in particular, topology and ODEs on the pure mathematics side, logic and set theory on the computer scientific side).

Outline of the course

1. Introduction. Abstract interpretation of subsets of R^n and of functions from R^m to R^n (i.e. set-based methods). Classical examples: intervals (boxes), zones, polyhedra, zonotopes, Application to outer-approximations of the image of a function f: R^m → R^n; Inner-approximations of the image of functions of arbitrary order.
2. Inner and outer approximation of general quantifier elimination, and applications (verification in the large, controller design etc.).
3. Abstract interpretation (inner and outer) for feedforward neural networks. Application to verification of simple properties, such as linear specifications and robustness.
4. (robust) Reachability problems for (uncertain) discrete dynamical systems ; (robust) Reachability problems for (uncertain) continuous dynamical systems (AI and non-AI controlled): Taylor models, reach-avoid properties through inner and outer-approximations.
5. Beyond finite time reachability: invariants through value iteration in an abstract domain, or through analytical means, constraint solving or quantifier elimination (Lyapunov functions). Extension of Lyapunov methods using finer geometrical properties (Wazewski property in particular).
6. More on the geometry of the reachability space: discretization of the reachable space and bisimulation with applications to controller design; simple topological complexity (for graphs in particular) and applications to the complexity of discrete time motion planning.
7. The geometry of the trajectory space: application to controllers of continuous dynamical systems that avoid sets of obstacles; The general (continuous) case of complexity of motion planning
8. The geometry of reachable states in coordination problems: optimal motion planners for coordination of multiple robots without collision. The fully general asynchronous case: impossibility of asynchronous gathering tasks.

We will also discuss more on research perspectives: internships, research directions in distributed computing, mobile robotics (average consensus, discrete algorithmics under various hypotheses), control, verification, AI… some last minute exciting developments.

Course format

The course will be given in 3-hour class sessions split in a 2-hour course with one break followed, after a second break, by a tutorial or an exercise session. Courses 1, 2, 3, 4 will be given by Sylvie Putot, courses 5, 6, 7, 8 by Eric Goubault. Some of the exercise sessions/tutorials may be given jointly by the two professors.

Exercise sessions will be rather classical, on paper exercices, with proofs to be fully written up by students; as for reading proposals, the principle is as follows: one group of students, in turn, prepares a presentation, the other groups also read the paper and will ask questions during the presentation of the first group (about limitations, applicability, theoretical aspects, related work they may have found etc.) as a preparation to research work.

Evaluation modalities

Session 1. Written exam in the classroom during the exam period at the end of the period. All written documents authorized. Final grade = max(E, (P+2E)/3), where E=exam grade, P=partial grade given to oral reading presentations.

Session 2. At the request of the students concerned. With few exceptions, session 2 is only granted to students who have passed and failed session 1. The format depends on particular cases, and may take the form of a written or oral exam, or another form. Session note 2 replaces session note 1 where applicable.

Related courses and dependencies

Main links:

• 2.3.1 Concurrence
• 2.6 Interprétation Abstraite
• 2.31.1 Calculabilité dans les systèmes multi-agents

Other related courses:

• 2.14.1 Géométrie et topologie algorithmiques
• 2.18.2 Algorithmique distribuée avec mémoire partagée et dans une moindre mesure, 2.18.1

References

[H96] Thomas A. Henzinger, The Theory of Hybrid Automata. LICS 1996.

[ACHH+95] Alur, Courcoubetis, Halbwachs, Henzinger, Ho, Nicollin, Olivero, Sifakis, Yovine, The algorithmic analysis of hybrid systems. TCS 1995.

[R05] R. Ghrist, J. O'Kane,and S. LaValle, Computing Pareto optimal coordinations on roadmaps, (posted 1/05), Intl. J. Robotics Research, 12(11), 997–1010, 2005.

[SIAM06] R. Ghrist and S. LaValle, Nonpositive curvature and Pareto-optimal coordination of robots, (posted 9/04, revised 2/06), SIAM J. Control & Optimization, 45(5), 1697–1713, 2006.

[EMS08] Michael Farber: Invitation to Topological Robotics (book). EMS 2008.

[OL08] Jason M. O’Kane, Steven M. LaValle, Comparing the Power of Robots. The International Journal of Robotic Research 2008.

[G12] Antoine Girard: Controller synthesis for safety and reachability via approximate bisimulation. Autom. 48(5): 947-953 (2012)

[HKR13] Maurice Herlihy, Dmitry Kozlov, Sergio Rajsbaum, Distributed Computing Through Combinatorial Topology. Morgan Kaufmann 2013.

[FMSD15] Eric Goubault, Sylvie Putot: A zonotopic framework for functional abstractions. Formal Methods Syst. Des. 47(3) (2015)

[FGHMR16] Lisbeth Fajstrup, Eric Goubault, Emmanuel Haucourt, Samuel Mimram, Martin Raussen, Directed Algebraic Topology and Concurrency Theory, Springer, 2016.

[SKJP16] Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, André Platzer, A Method for Invariant Generation for Polynomial Continuous Systems. VMCAI 2016.

[NIPS18] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Puschel, Martin Vechev, Fast and Effective Robustness Certification. NIPS 2018.

[HSCC19] Eric Goubault, Sylvie Putot: Inner and outer reachability for the verification of control systems. HSCC 2019

[DC19] Manuel Alcantara, Armando Castañeda, David Flores-Peñaloza, Sergio Rajsbaum: The topology of look-compute-move robot wait-free algorithms with hard termination. Distributed Comput. 32(3): 235-255 (2019)

[IEEE20] Eric Goubault, Sylvie Putot: Robust Under-Approximations and Application to Reachability of Non-Linear Control Systems With Disturbances.IEEE Control. Syst. Lett. 4(4): 928-933 (2020)

[APCT20] Eric Goubault, Michael Farber, Aurélien Sagnier: Directed topological complexity. J. Appl. Comput. Topol. 4(1) (2020)

[LMCS20] Eric Goubault, Samuel Mimram: Directed Homotopy in Non-Positively Curved Spaces. Log. Methods Comput. Sci. 16(3) (2020)

[ADHS21] Eric Goubault, Sylvie Putot: Tractable higher-order under-approximating AE extensions for non-linear systems. ADHS 2021

[IC21] Laurent Fribourg, Eric Goubault, Sameh Mohamed, Marian Mrozek, Sylvie Putot: A topological method for finding invariant sets of continuous systems. Inf. Comput. 277: 104581 (2021)

[OLGB21] Carlos Ortiz, Adriana Lara, Jesus Gonzalez, Ayse Borat, “A Randomized Greedy Algorithm for Piecewise Linear Motion Planning, Mathematics 2021.

[ICWA21] Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, Verisig 2.0: Verification of Neural Network Controllers using Taylor Model Preconditioning. CAV 2021.

[CAV22] Eric Goubault, Sylvie Putot: RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems. CAV 2022

[LKB23] Ertai Luo, Niklas Kochdumper, Stanley Bak, Reachability Analysis for Linear Systems with Uncertain Parameters using Polynomial Zonotopes. HSCC 2023.

[MATH23] Yuliy Baryshnikov: Linear Obstacles in Linear Systems and Ways to Avoid Them. Adv. Appl. Math. Vol. 151, 2023

[HSCC24] Eric Goubault, Sylvie Putot: Inner and outer approximate quantifier elimination for general reachability problems. HSCC 2024

[LM24] Tobias Ladner, Matthias Althoff, Exponent Relaxation of Polynomial Zonotopes and Its Applications in Formal Neural Network Verification. AAAI 2024.

[KSA24] Adrian Kulmburg, Lukas Schäfer, and Matthias Althoff, Approximability of the Containment Problem for Zonotopes and Ellipsotopes. ArXiv 2024.

[BGS24] Guillaume Berger, Masoumeh Ghanbarpour, Sriram Sankaranarayanan, Cone-Based Abstract Interpretation for NonLinear Positive Invariant Synthesis. HSCC 2024.

[RJD24] Wei Ren, Raphael M. Jungers, Dimos V. Domarogonas, Zonotope-based Symbolic Controller Synthesis for Linear Temporal Logic Specifications. IEEE Transactions on Automatic Control 2024.