From Propositional to First-Order Monitoring - Runtime Verification - page 59

From Propositional to First-Order Monitoring

Andreas Bauer 1 , 2 , Jan-Christoph Kuster 1 , 2 , and Gil Vegliach 1

1 NICTA Software Systems Research Group
2 Australian National University

Abstract. The main purpose of this paper is to introduce a first-order temporal
logic, LTL FO , and a corresponding monitor construction based on a new type of
automaton, called spawning automaton.
Specifically, we show that monitoring a specification in LTL FO boils down to
an undecidable decision problem. The proof of this result revolves around specific
ideas on what we consider a “proper” monitor. As these ideas are general, we out-
line them first in the setting of standard LTL, before lifting them to the setting of
first-order logic and LTL FO . Although due to the above result one cannot hope to
obtain a complete monitor for LTL FO , we prove the soundness of our automata-
based construction and give experimental results from an implementation. These
seem to substantiate our hypothesis that the automata-based construction leads to
efficient runtime monitors whose size does not grow with increasing trace lengths
(as is often observed in similar approaches). However, we also discuss formulae
for which growth is unavoidable, irrespective of the chosen monitoring approach.

1 Introduction

In the area of runtime verification (cf. [17,16,12,8]), a monitor typically describes a de-
vice or program which is automatically generated from a formal specification capturing
undesired (resp. desired) system behaviour. The monitor's task is to passively observe
a running system in order to detect if the behavioural specification has been satisfied
or violated by the observed system behaviour. While, arguably, the majority of runtime
verification approaches are based on propositional logic (or expressively conservative
parametric extensions thereof; cf.

§

6 for an overview), there exist works that have con-
sidered full first-order logic (cf. [16,5,4]). Monitoring first-order specifications has also
gained prior attention in the database community, especially in the context of so called
temporal triggers, which correspond to first-order temporal logic specifications that are
evaluated wrt. a linear sequence of database updates (cf. [10,11,23]). Although the un-
derlying logics are generally undecidable, the monitors in these works usually address
decidable problems, such as “is the so far observed behaviour a violation of a given
specification ϕ ?” Additionally, in many approaches, ϕ must only ever be a safety or do-
main independent property for this problem to actually be decidable (cf. [10,4]), which
can be ensured by syntactic restrictions on the input formula, for example.

NICTA is funded by the Australian Government as represented by the Department of Broad-
band, Communications and the Digital Economy and the Australian Research Council through
the ICT Centre of Excellence program.