Predictive Monitoring against Pattern Regular Languages

TL;DR

The paper tackles the problem of analyzing concurrent software against high-level temporal specifications via predictive runtime monitoring under reorderings modeled by trace equivalence. It focuses on specifications expressed as regular languages and proves a super-linear lower bound of $O(n^α)$ for the general predictive problem, indicating that efficient solutions are unlikely in full generality. To enable practical deployment, it identifies pattern languages (and generalized pattern languages) as a tractable subclass that can express specific event orderings and demonstrates a constant-space streaming linear-time algorithm for predictive monitoring in this setting. This work thus delineates the computational limitations of predictive monitoring and offers a practical, scalable approach for a meaningful subset of temporal properties with direct relevance to runtime verification of concurrent systems.

Abstract

In this paper, we focus on the problem of dynamically analysing concurrent software against high-level temporal specifications. Existing techniques for runtime monitoring against such specifications are primarily designed for sequential software and remain inadequate in the presence of concurrency -- violations may be observed only in intricate thread interleavings, requiring many re-runs of the underlying software. Towards this, we study the problem of predictive runtime monitoring, inspired by the analogous problem of predictive data race detection studied extensively recently. The predictive runtime monitoring question asks, given an execution $σ$, if it can be soundly reordered to expose violations of a specification. In this paper, we focus on specifications that are given in regular languages. Our notion of reorderings is trace equivalence, where an execution is considered a reordering of another if it can be obtained from the latter by successively commuting adjacent independent actions. We first show that the problem of predictive admits a super-linear lower bound of $O(n^α)$, where $n$ is the number of events in the execution, and $α$ is a parameter describing the degree of commutativity. As a result, predictive runtime monitoring even in this setting is unlikely to be efficiently solvable. Towards this, we identify a sub-class of regular languages, called pattern languages (and their extension generalized pattern languages). Pattern languages can naturally express specific ordering of some number of (labelled) events, and have been inspired by popular empirical hypotheses, the `small bug depth' hypothesis. More importantly, we show that for pattern (and generalized pattern) languages, the predictive monitoring problem can be solved using a constant-space streaming linear-time algorithm.