Wed 19 Jan 2022 17:05 - 17:30 at Salon I - Algorithmic Verification 2 Chair(s): Qirun Zhang

We consider the MSO model-checking problem for simple linear loops, or equivalently discrete-time linear dynamical systems, with semialgebraic predicates. We place no restrictions on the number of variables, or equivalently the ambient dimension. We establish decidability of the model-checking problem provided that each semialgebraic predicate either has intrinsic dimension $1$, or is contained within some three-dimensional subspace.

Wed 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:40 - 17:30
Algorithmic Verification 2POPL at Salon I
Chair(s): Qirun Zhang Georgia Institute of Technology
Research paper
Context-Bounded Verification of Thread PoolsRemote
DOI Media Attached
Research paper
What’s Decidable about Linear Loops?InPerson
Toghrul Karimov MPI-SWS, Engel Lefaucheux MPI-SWS, Joël Ouaknine MPI-SWS, David Purser MPI-SWS, Anton Varonka MPI-SWS, Markus A. Whiteland MPI-SWS, James Worrell University of Oxford
DOI Pre-print Media Attached