2020/10/27 by Shaull Almagor, Almagor, Shaull, Toghrul Karimov +7
Computer Science · Mathematics · #Advanced Topology and Set Theory #Computability, Logic, AI Algorithms #F.3.1 #F.4.1 #FOS: Computer and information sciences #FOS: Electrical engineering #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Rings, Modules, and Algebras #Systems and Control (eess.SY) #electronic engineering #information engineering #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2010.14432
openalex publication_date 2020/10/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider the problem of deciding ω-regular properties on infinite traces produced by linear loops. Here we think of a given loop as producing a single infinite trace that encodes information about the signs of program variables at each time step. Formally, our main result is a procedure that inputs a prefix-independent ω-regular property and a sequence of numbers satisfying a linear recurrence, and determines whether the sign description of the sequence (obtained by replacing each positive entry with "+", each negative entry with "-", and each zero entry with "0") satisfies the given property. Our procedure requires that the recurrence be simple, \ie, that the update matrix of the underlying loop be diagonalisable. This assumption is instrumental in proving our key technical lemma: namely that the sign description of a simple linear recurrence sequence is almost periodic in the sense of Muchnik, Semënov, and Ushakov. To complement this lemma, we give an example of a linear recurrence sequence whose sign description fails to be almost periodic. Generalising from sign descriptions, we also consider the verification of properties involving semi-algebraic predicates on program variables.