A theory of register monitors Conference Paper

Author(s): Ferrère, Thomas; Henzinger, Thomas A; Saraç, Ege N
Title: A theory of register monitors
Title Series: ACM/IEEE Symposium on Logic in Computer Science
Affiliation IST Austria
Abstract: The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation 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 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 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety -languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation 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 as expressive as real-time Turing machines.
Keywords: Reactive system; Computer circuits; Adders; Turing machines; Infinite state; Instruction set; Real time monitors; Register machines; Safety violations; Sequence of events; Unbounded memory
Conference Title: LICS: Logic in Computer Science
Volume: Part F138033
Conference Dates: 9 - 12 July, 2018
Conference Location: Oxford, UK
ISBN: 10436871 (ISSN); 9781450355834 (ISBN); 9781450355834 (ISBN)
Publisher: IEEE  
Date Published: 2018-07-09
Start Page: 394
End Page: 403
DOI: 10.1145/3209108.3209194
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work