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 |