@article{10.1145/3498727,
    Abstract = {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 equivalently the ambient dimension. We establish decidability of the model-checking problem provided that each semialgebraic predicate either has intrinsic dimension at most 1, or is contained within some three-dimensional subspace. We also note that lifting either of these restrictions and retaining decidability would necessarily require major breakthroughs in number theory.},
    Address = {New York, NY, USA},
    Author = {Karimov, Toghrul and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Purser, David and Varonka, Anton and Whiteland, Markus A. and Worrell, James},
    File = {What’s Decidable about Linear Loops? - 3498727 - p.pdf},
    Journal = {Proc. ACM Program. Lang.},
    Keywords = {linear dynamical systems, verification, MSO model checking},
    Month = {jan},
    Number = {POPL},
    Publisher = {Association for Computing Machinery},
    Title = {What's Decidable about Linear Loops?},
    URL = {https://doi.org/10.1145/3498727},
    Volume = {6},
    Year = {2022},
    articleno = {65},
    bdsk-url-1 = {https://doi.org/10.1145/3498727},
    date-added = {2022-01-17 07:58:57 +0100},
    date-modified = {2022-01-17 07:58:57 +0100},
    issue_date = {January 2022},
    numpages = {25},
    doi = {10.1145/3498727}
}

@article{10.1145/3498727, Abstract = {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 equivalently the ambient dimension. We establish decidability of the model-checking problem provided that each semialgebraic predicate either has intrinsic dimension at most 1, or is contained within some three-dimensional subspace. We also note that lifting either of these restrictions and retaining decidability would necessarily require major breakthroughs in number theory.}, Address = {New York, NY, USA}, Author = {Karimov, Toghrul and Lefaucheux, Engel and Ouaknine, Jo\"{e}l and Purser, David and Varonka, Anton and Whiteland, Markus A. and Worrell, James}, File = {What’s Decidable about Linear Loops? - 3498727 - p.pdf}, Journal = {Proc. ACM Program. Lang.}, Keywords = {linear dynamical systems, verification, MSO model checking}, Month = {jan}, Number = {POPL}, Publisher = {Association for Computing Machinery}, Title = {What's Decidable about Linear Loops?}, URL = {https://doi.org/10.1145/3498727}, Volume = {6}, Year = {2022}, articleno = {65}, bdsk-url-1 = {https://doi.org/10.1145/3498727}, date-added = {2022-01-17 07:58:57 +0100}, date-modified = {2022-01-17 07:58:57 +0100}, issue_date = {January 2022}, numpages = {25}, doi = {10.1145/3498727} }