Monitoring First-order Parametric Linear-time Temporal Logic
Kai Hornung
Linear-time temporal logic (LTL) is a widely used formalism to express specifications for runtime verification. By extending LTL with parameters (PLTL), monitoring algorithms cannot only be used to verify behaviour, but also to collect data on how long certain properties hold or how long it takes for a system to fulfil a property. The fact that LTL (and PLTL) usually work with atomic propositions to express a system’s condition is debilitating, since specifications may also depend on data – e.g. values of variables or measurements to verify internal consistency – which is hard to model using solely absence and presence of properties expressed as atomic propositions. This work is dedicated to address this problem by first extending PLTL with data and afterwards constructing a corresponding monitoring algorithm that also takes care of obtaining measurements for the included parameters. In order to incorporate data, the atomic propositions in PLTL will be replaced by predicates over an arbritrary, possibly infinite domain. Universally quantified variables ranging over this domain will facilitate the construction and readability of data-aware specifications, lifting PLTL up to a first-order logic called First-order PLTL (FO-PLTL). Then, an online monitoring algorithm for measuring a system’s behaviour using FO-PLTL specifications is presented, together with the corresponding implementation that shows detailed measuring capabilities.
Bachelor Thesis.