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...

Cijeli opis

Bibliografski detalji
Glavni autori: Karimov, T, Lefaucheux, E, Ouaknine, J, Purser, D, Varonka, A, Whiteland, MA, Worrell, J
Format: Conference item
Jezik:English
Izdano: Association for Computing Machinery 2022

Slični predmeti