Efficient, Expressive, and Verified Temporal Query Evaluation

Runtime monitoring (or runtime verification) is an approach to checking compliance of a system’s execution with a specification (e.g., a temporal query). The system’s execution is logged into a trace—a sequence of time-points, each consisting of a time-stamp and observed events. A monitor is an algorithm that produces verdicts on the satisfaction of a temporal query on a trace. This thesis develops new monitoring algorithms for expressive temporal query languages that are more time- and space-efficient than the state-of-the-art and produce detailed verdicts. An online monitor reads the trace forwards, one time-point after another. An offline monitor processes the time-points in an arbitrary order. We propose a novel paradigm—multi-head monitoring—that fills a middle-ground between online and offline monitoring. A multi-head monitor uses multiple reading heads that read the trace forwards. We develop multi-head monitors for metric temporal logic (MTL) and metric dynamic logic (MDL). Our monitors improve upon the state-of-the-art by optimizing the time and space complexity while producing a sequence of Boolean verdicts denoting the temporal query’s satisfaction at every time-point. We have implemented our monitors, empirically confirmed that their performance improves upon existing approaches, and formally verified the correctness of our monitors using the Isabelle/HOL proof assistant. MTL and MDL events cannot have parameters and queries cannot contain variables. Metric first-order temporal logic (MFOTL) generalizes MTL with parametric events and first-order variables ranging over an arbitrary domain. Hence, a monitor evaluates an MFOTL query at every time-point to a relation representing the valuations of the free variables satisfying the query. An online monitor for MFOTL had been developed in previous work and later formally verified using Isabelle/HOL. The formally verified monitor is called VeriMon. In this thesis, we optimize the time complexity of evaluating VeriMon’s Since and Until temporal operators. Query evaluation for a proper subset of MFOTL queries can be efficiently implemented using relational algebra operations. Alternatively, an arbitrary MFOTL query can be evaluated using structures that represent arbitrary relations satisfying the subqueries of the query, e.g., automatic structures or binary decision diagrams. However, these alternative representations have a negative impact on the performance of the resulting monitor. Hence, in this thesis we use relational algebra operations to evaluate an arbitrary MFOTL query. We first investigate the case of relational calculus (RC), i.e., MFOTL without temporal operators. We develop a novel approach to RC query evaluation by translating an arbitrary RC query into a pair of relational algebra normal form (RANF) queries that can be evaluated using relational algbra operations on finite tables: one characterizes the original query’s relative safety (i.e., whether it evaluates to a finite relation) and the other one is equivalent to the original query if the original query is relatively safe. We implement our translation and empirically confirm that the performance of evaluating the queries produced by our translation improves upon existing approaches to RC query evaluation. Finally, we generalize our translation of RC queries to MFOTL queries. This way, we obtain a monitor for an arbitrary MFOTL query that decides for every time-point if it evaluates to a finite relation and computes the relation if it is finite