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 JanDisplayed time zone: Eastern Time (US & Canada) change
16:40 - 17:30
|Context-Bounded Verification of Thread PoolsRemote|
Pascal Baumann MPI-SWS, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam MPI-SWS, Georg Zetzsche MPI-SWSDOI Media Attached
|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 OxfordDOI Pre-print Media Attached