Toric words improve checking system behaviors in noisy conditions
Model Checking for Noisy Toric Words
Formal Languages and Automata TheoryLogic in Computer Science
Summary
Checking if complex systems behave as expected can be hard, especially when there is uncertainty or noise. This paper studies a special way of describing system behaviors called toric words and extends it to handle noisy data. The authors show that their noisy model keeps key repeating patterns that help in deciding whether a system’s behavior matches certain rules. They also prove it’s possible to decide membership in certain pattern languages for systems following these noisy models.
What this means in practice
- •For software verification teams: Decide if system executions with uncertain or noisy signals meet complex temporal specifications using the theory of noisy toric words.
- •For control systems engineers: Analyze recurrent behaviors of linear loop systems under noise to verify operational properties accurately.
A theory result. No direct application yet.
Authors
Mihir Vahanwala
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.