Invariant Synthesis for Linear Dynamical Systems - Pierre Ohlmann, ENS de Lyon

Explore the intricacies of invariant synthesis for linear dynamical systems in this 49-minute lecture by Pierre Ohlmann from ENS de Lyon, presented at the Alan Turing Institute. Delve into the Orbit Problem, which involves determining whether the orbit of a vector under repeated applications of a linear transformation can reach a specific target vector. Examine the problem from a novel perspective, focusing on synthesizing suitable invariants as subsets of the vector space that contain the initial vector but not the target. Learn about the existence of semialgebraic invariants in most cases and the decidability of semilinear invariant existence. Discover the connection between this work and static analysis, and explore related concepts such as Jordan blocks, Jordan form, and polyhedral invariants. Gain insights into the application of these techniques to diagonal behavior and examine practical examples to solidify understanding.

Introduction
The orbit problem
Static analysis
Problem definition
Motivation
Polyhedral invariants
Main results
Jordan blocks
Jordan form
Invariant for the whole matrix
Invariant for a convenient block
Diagonal behavior
Invariant
Example
Related problems