Abstract
This paper investigates monitorability in the context of probabilistic systems. We specify how monitor verdicts, reached over finite (partial) traces, can be given a probabilistic interpretation. For monitors that are used to verify properties at runtime, we also relate their probabilistic verdicts to the probability that a trace satisfies the property of interest. This leads us to define probabilistic monitor soundness and completeness, which are then used to formulate probabilistic monitorability. Surprisingly, we show that the resulting notions coincide with standard monitorability definitions from the literature. This allows us to transfer prior results from the standard setting to the probabilistic realm.
| Original language | English |
|---|---|
| Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Publisher | Springer, Cham |
| Pages | 325-342 |
| Number of pages | 18 |
| ISBN (Electronic) | 978-3-031-22337-2 |
| ISBN (Print) | 978-3-031-22336-5 |
| DOIs | |
| Publication status | Published - 2022 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 13660 LNCS |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Bibliographical note
Funding Information:This research was supported by the projects ‘TheoFoMon: Theoretical Foundations for Monitorability’ (no. 163406-051), ‘Open Problems in the Equational Logic of Processes (OPEL)’ (no. 196050-051) and ‘MoVeMnt: Mode(l)s of Verification and Monitorability’ (no. 217987-051) of the Icelandic Research Fund, project BehAPI, funded by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant (no. 778233), and the Italian MIUR project PRIN 2017FTXR7S IT MATTERS ‘Methods and Tools for Trustworthy Smart Systems’.
Publisher Copyright:
© 2022, Springer Nature Switzerland AG.