A Note on Runtime Verification of Concurrent Systems

TL;DR

This paper proposes a trace-based logic approach for runtime verification of concurrent systems, enabling implicit consideration of all equivalent interleavings through partial-order representations and a three-valued logic monitor.

Contribution

It introduces a three-valued version of Linear Temporal Logic over Mazurkiewicz Traces (LTrL) and a monitor synthesis method for concurrent system verification.

Findings

Trace-consistent B"uchi automata construction for LTrL

Three-valued logic for runtime monitoring

Monitors yield consistent verdicts for all linearizations

Abstract

To maximize the information gained from a single execution when verifying a concurrent system, one can derive all concurrency-aware equivalent executions and check them against linear specifications. This paper offers an alternative perspective on verification of concurrent systems by leveraging trace-based logics rather than sequence-based formalisms. Linear Temporal Logic over Mazurkiewicz Traces (LTrL) operates on partial-order representations of executions, meaning that once a single execution is specified, all equivalent interleavings are implicitly considered. This paper introduces a three valued version of LTrL, indicating whether the so-far observed execution of the concurrent system is one of correct, incorrect or inconclusive, together with a suitable monitor synthesis procedure. To this end, the paper recalls a construction of trace-consistent B\"uchi automata for LTrL formulas and explains how to employ it in well-understood monitor synthesis procedures. In this way, a monitor results that yields for any linearization of an observed trace the same verification verdict.