A Note on Runtime Verification of Concurrent Systems

@inproceedings {1497,
	title = {A Note on Runtime Verification of Concurrent Systems},
	booktitle = {Principles of Formal Quantitative Analysis - Essays Dedicated to Christel Baier on the Occasion of Her 60th Birthday},
	series = {Lecture Notes in Computer Science},
	volume = {15760},
	year = {2025},
	publisher = {Springer},
	organization = {Springer},
	abstract = {<p>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{\"u}chi 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.</p>
},
	doi = {10.1007/978-3-031-97439-7_12},
	url = {https://doi.org/10.1007/978-3-031-97439-7_12},
	author = {Martin Leucker},
	editor = {Nathalie Bertrand and Clemens Dubslaff and Sascha Kl{\"u}ppelholz}
}