A New Syntax and Semantics for Probabilistic Trace Expressions

Abstract

Runtime Verification (RV) techniques are typically defined under the assumption of complete observability of system executions. In many realistic settings, however, monitors must operate under partial observability, where events may be lost, delayed, or unobservable. This raises fundamental questions about how to interpret specifications, verdicts, and uncertainty during monitoring. In this paper, we propose a new syntax and semantics for Probabilistic Trace Expressions (PTEs), a formal framework that integrates probabilistic reasoning into the operational semantics of Trace Expressions. Trace Expressions (TE) are a highly expressive specification formalism for runtime verification that we started to develop 15 years ago. Rather than attaching probabilities to syntactic transitions, as we did in the original formulation of PTEs dating back 2022, probabilities are now associated with the set of event types enabled in each semantic state, ensuring semantic consistency beyond finite-state models, and high modularity of the PTE specification. The PTE framework supports principled reasoning about missing events (gaps), distinguishes between observational and generative probabilistic interpretations -- which represents a more refined semantics w.r.t. the original PTE formulation of 2022 -- and subsumes classical probabilistic models such as Hidden Markov Models. We discuss how PTEs enable belief-based monitoring under uncertainty, illustrate their use in one representative Mars Rover scenario, and reflect on the conceptual implications for runtime verification in partially observable environments.