What’s decidable about linear loops?

Karimov, Toghrul ORCID: 0000-0002-9405-2332, Lefaucheux, Engel ORCID: 0000-0003-0875-300X, Ouaknine, Joël ORCID: 0000-0003-0031-9356, Purser, David ORCID: 0000-0003-0394-1634, Varonka, Anton ORCID: 0000-0001-5758-0657, Whiteland, Markus A ORCID: 0000-0002-6006-9902 and Worrell, James ORCID: 0000-0001-8151-2443 (2022) What’s decidable about linear loops? Proceedings of the ACM on Programming Languages, 6 (POPL). pp. 1-25.

Access the full-text of this item by clicking on the Open Access link.

Official URL: http://dx.doi.org/10.1145/3498727

Abstract

<jats:p> 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 <jats:italic>either</jats:italic> has intrinsic dimension at most 1, <jats:italic>or</jats:italic> 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. </jats:p>

Item Type:	Article
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	29 Mar 2023 10:34
Last Modified:	15 Mar 2024 19:59
DOI:	10.1145/3498727
Open Access URL:	http://dx.doi.org/10.1145/3498727
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3169334