Eric Goubault, LIX & École Polytechnique goubault@lix.polytechnique.fr

Sylvie Putot, LIX & École Polytechnique putot@lix.polytechnique.fr

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, and the development of verification techniques relying on variants and invariants inspired from Lyapunov functions and reachability methods. More recently, the second advent of artificial intelligence has fostered new fruitful interactions with formal methods, in particular when neural networks are used in the feedback control loop, for instance for perception or in place of more classical controllers.

In control, where continuous mathematics plays a big role, the geometry of the state space and of the set of possible trajectories is naturally considered, for all application purposes. Set-based reachability analysis, extending abstract interpretation domains (polyhedra, zonotopes, ellipsoids etc.) for controlled systems, synthesize guaranteed approximations of tubes of possible trajectories, under possibly complicated interactions between control and disturbances. A finer geometric knowledge (e.g. algebraic topological invariants) about these sets buys you more, 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.

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

The course takes place on Tuesday 8h45-11h45 in Room 1004 of the Sophie Germain building.

Each course provides a specific bibliography in the course slides. The 3-hour class sessions include an exercise session or paper presentation and discussion.

• [09/12] Introduction slides Set-based methods and abstract interpretation slides [SP]
  • reading assignment: E. Goubault and S. Putot, A zonotopic framework for functional abstractions, Formal Methods in System Design, 2016 link
• [16/12] Abstraction-based verification of neural networks slides [SP]
  • reading assignment: M. Forets and C. Schilling, The inverse problem for neural networks, Arxiv 2023 link
  • exercice (easy): link, solution
• [06/01] Reachability verification of controlled and hybrid systems [SP]
• [13/01] no course
• [20/01] Inner and outer approximations of general quantified problems and applications [SP]
• [27/01] Beyond finite time reachability, and homotopy theory [EG]
• [03/02] The geometry of the backward reach-avoid set, topological complexity and cohomology theory [EG]
• [10/02] The geometry of neural networks, quality of classification and persistent homology [EG]
• [17/02] The geometry of reachable states in coordination problems, if time permits [EG]
• [03/03] Written exam

Written exam at the end of the period. Written documents are authorized.

Basic knowledge of bachelor level mathematics and computer science.

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

1. Beyond finite time reachability: Lyapunov methods revisited using the geometry of the flow. Introduction to homotopy theory and to Conley theory, for dynamical systems and differential inclusions. Application to the existence of invariant sets, periodic orbits, and controllability.
2. More on the geometry of the reachability space: topology of the control space that ensures reach-avoid properties (see as a backward reach-avoid set). Complexity and simple topological complexity with applications to the complexity of motion planning.
3. The geometry of neural networks. Introduction to homology, cohomology and persistent homology. Application to the quality of a neural network as a classifier, and to the complexity of classification of data.
4. If time permits, we will cover some aspects of the geometry of reachable states in coordination problems: optimal motion planners for coordination of multiple robots without collision, and the fully general asynchronous case: impossibility of asynchronous gathering tasks.

Below are some references for the 2nd part of the course, starting with the online textbook Algebraic Topology by Allen Hatcher.

• Course 5:

- [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)

• Course 6-7:

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

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

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

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

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

• Course 8 (if time permits)

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

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

- [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)

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