What's decidable about linear loops?

We consider the MSO model-checking problem for simple linear loops, or equivalently discrete-time linear dynamical systems, with semialgebraic predicates (i.e., Boolean combinations of polynomial inequalities on the variables). We place no restrictions on the number of program variables, or equivale...

ver descrição completa

Detalhes bibliográficos
Main Authors: Karimov, T, Lefaucheux, E, Ouaknine, J, Purser, D, Varonka, A, Whiteland, MA, Worrell, J
Formato: Conference item
Idioma:English
Publicado em: Association for Computing Machinery 2022

Registos relacionados