Ain’t No Stopping Us Monitoring Now (extended abstract)
Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usually discarded. In this work, we carry out an in-depth analysis on monitorability, and how non-monitorable properties can still be partially verified. We present our theoretical results at a semantic level, without focusing on a specific formalism. Then, we show how our theory can be applied to achieve partial runtime verification of linear time properties expressed by concrete formalisms such as LTL.
| Ain’t No Stopping Us Monitoring Now - Slides (Ain’t No Stopping Us Monitoring Now.pdf) | 176KiB |
Fri 4 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:45 | |||
14:00 60mKeynote | Tell Me The Future, Correctly: On The Monitorability of Timed Logics Over Infinite Executions VORTEX | ||
15:00 30mTalk | Ain’t No Stopping Us Monitoring Now (extended abstract) VORTEX Luca Ciccone University of Turin, Francesco Dagnino , Angelo Ferrando University of Modena and Reggio Emilia File Attached | ||