Model Checking for Noisy Toric Words

Abstract

Toric words have recently gained attention as a means to model the behaviour of dynamical systems such as linear loops. This work is concerned with describing when the toric model is precise enough to decide whether the trace of a system is contained in an omega-regular language. Our contributions are threefold. (i) We use topological means to generalise a class of toric words by defining noise-robust dynamical systems and their sets of noisy traces. We prove that all noisy traces of a system are almost-periodic, and have the same set of recurrent factors. (ii) We apply the abstract techniques above to concrete sequences obtained as sign descriptions of real algebraic linear recurrence sequences (LRS), and show that the language-membership problem for sign descriptions of LRS with few dominant roots is decidable. (iii) We show that noisy traces of noise-robust dynamical systems are indistinguishable to a prefix-independent omega-regular language, and inclusion is decidable provided the common language of their recurrent factors is recursive. We incidentally obtain properties of prefix-independent omega-regular languages that may be of independent interest.