ECOOP 2026
Mon 29 June - Fri 3 July 2026 Brussels, Belgium
Tue 30 Jun 2026 16:25 - 16:50 at I.1.07 - Afternoon Session 2 (talks)

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 unob- servable. 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 probabilis- tic reasoning into the operational semantics of Trace Expressions. Trace Expressions (TE) are a highly expressive specification formal- ism 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, probabili- ties 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 proba- bilistic 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, il- lustrate their use in one representative Mars Rover scenario, and reflect on the conceptual implications for runtime verification in partially observable environments.

Tue 30 Jun

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 17:30
Afternoon Session 2 (talks)VORTEX at I.1.07
16:00
25m
Talk
Runtime Semantic Discovery for Evolving Action Alphabets
VORTEX
Pietro Bernabei Scuola IMT Alti Studi Lucca, University of Florence, Rosario Pugliese University of Florence
16:25
25m
Talk
A New Syntax and Semantics for Probabilistic Trace Expressions
VORTEX
Davide Ancona DIBRIS, University of Genova, Italy, Angelo Ferrando , Viviana Mascardi DIBRIS, University of Genova, Italy
16:50
25m
Talk
Spatial Logic of Directed Graphs
VORTEX
Giorgio Audrito Università di Torino, Gianluca Aguzzi Alma Mater Studiorum - Università di Bologna, Ferruccio Damiani University of Turin, Gianluca Torta giatorta@gmail.com, Volker Stolz Høgskulen på Vestlandet