FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A Theory of Register Monitors

Authors: Thomas Ferrère, Thomas A Henzinger and N Ege Sarac

Paper Information

Title:A Theory of Register Monitors
Authors:Thomas Ferrère, Thomas A Henzinger and N Ege Sarac
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:monitoring, register machines, expressiveness, omega-languages, real-time
Abstract:

ABSTRACT. The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of an error in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these {\em register monitors} according to the number $k$ of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every $k>1$, monitors with $k+1$ counters (with instruction set $\langle +1,= \rangle$) are strictly more expressive than monitors with $k$ counters: there is a safety $\omega$-language $L_k$ such that the finite prefixes not in $L_k$ can be recognized on-line with $k+1$ but not with $k$ counters. We also show that adder monitors (with instruction set $\langle 1,+,= \rangle$) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety $\omega$-languages for $k=6$. {\em Real-time monitors} are further required to signal the occurrence of an error as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are at least as expressive as the model of real-time Turing machines studied in the 1960s.

Pages:10
Talk:Jul 12 14:20 (Session 76E)
Paper: