Abstract. This paper addresses the problem of safely navigating a mobile robot with limited sensing capability and limited information about stationary obstacles. We consider two s...
Dung Phan, Junxing Yang, Denise Ratasich, Radu Gro...
Abstract. Although runtime monitoring is a promising technique to improve the veriļ¬cation of complex safety-critical systems, the general design trend towards utilizing black-box...
Aaron Kane, Omar Chowdhury, Anupam Datta, Philip K...
Continuous and hybrid behaviors naturally arise from many dynamical systems. In this tutorial, we present state-of-the-art techniques for qualitative and quantitative reasoning abo...
Abstract. The problem of estimating quantitative properties of distributed cyber-physical software that coordinate and adapt to uncertain environments is addressed. A domain-speciļ...
Ultra-critical systems are growing more complex, and future systems are likely to be autonomous and cannot be assured by traditional means. Runtime Veriļ¬cation (RV) can act as th...
We study ĀµHML (a branching-time logic with least and greatest ļ¬xpoints) from a runtime veriļ¬cation perspective. We establish which subset of the logic can be veriļ¬ed at runt...
Abstract. Requirements of cyberphysical systems (CPS) can be rigorously speciļ¬ed using Signal Temporal Logic (STL). STL comes equipped with semantics that are able to quantify ho...
In the most comprehensive study on Android attacks so far (undertaken by the Android Malware Genome Project), the behaviour of more than 1, 200 malwares was analysed and categorise...
Abstract. We address the speciļ¬cation and veriļ¬cation of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator ca...
Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Mi...
Abstract. Parametric runtime veriļ¬cation is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper considers t...