If At First You Don't Succeed: Extended Monitorability through Multiple Executions
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910955977310208 |
|---|---|
| author | Achilleos, Antonis Francalanza, Adrian Xuereb, Jasmine |
| author_facet | Achilleos, Antonis Francalanza, Adrian Xuereb, Jasmine |
| contents | This paper studies the extent to which branching-time properties can be adequately verified using runtime monitors. We depart from the classical setup where monitoring is limited to a single system execution and investigate the enhanced observational capabilities when monitoring a system over multiple runs. To ensure generality in our results, we focus on branching-time properties expressed in the modal mu-calculus, a well-studied foundational logic that is used by state-of-the-art model checkers. Our results show that the proposed setup can systematically extend previously established monitorability limits for branching-time properties. We then validate our results by instantiating them to verify actor-based systems. We also prove bounds that capture the correspondence between the syntactic structure of a property and the number of required system runs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_05229 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | If At First You Don't Succeed: Extended Monitorability through Multiple Executions Achilleos, Antonis Francalanza, Adrian Xuereb, Jasmine Logic in Computer Science This paper studies the extent to which branching-time properties can be adequately verified using runtime monitors. We depart from the classical setup where monitoring is limited to a single system execution and investigate the enhanced observational capabilities when monitoring a system over multiple runs. To ensure generality in our results, we focus on branching-time properties expressed in the modal mu-calculus, a well-studied foundational logic that is used by state-of-the-art model checkers. Our results show that the proposed setup can systematically extend previously established monitorability limits for branching-time properties. We then validate our results by instantiating them to verify actor-based systems. We also prove bounds that capture the correspondence between the syntactic structure of a property and the number of required system runs. |
| title | If At First You Don't Succeed: Extended Monitorability through Multiple Executions |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2306.05229 |