The speaker for this week’s seminar is our own Margret. Please find the title and abstract below.

Title Safety Verification for Discrete-Time Linear Systems over Real Data

Abstract We study safety (trapped-orbit) verification for discrete-time linear systems $x_{k+1}=\mathbf A x_k$ with a compact regular-closed guard $K\subseteq\mathbb R^n$ and nonempty interior $K^\circ$, in the bit-model setting of real computation. Under a spectral promise ($|\lambda|\le 1$ for all eigenvalues and a given gap $\delta>0$ with $|\lambda|\ge 1-\delta\Rightarrow |\lambda|=1$), we show these problems are as close to decidable as one can expect over real data: there are sound partial algorithms for (Problem~A) given-point trapping and (Problem~B) existence of an interior trapped point, which halt exactly on robust yes-instances. Whenever they halt, they output a finite certificate consisting of a trapped point and a finite rational cover of a compact forward-invariant set contained in $K^\circ$; when they do not halt, arbitrarily small perturbations force escape (Problem~A) or eliminate all interior trapped points (Problem~B).