Controlling and designing spatio-temporal behaviours requires proper formal tools to describe such properties, and to monitor and verify whether, and how robustly, they are satisfied by a system. In this talk, we introduce Signal Spatio-Temporal Logic (SSTL), a modal logic to describe spatio-temporal properties, equipped with a boolean and a quantitative semantics, and monitoring algorithms for spatio-temporal trajectories. We will also present jSSTL, a Java tool for the specification of SSTL properties. We describe the logical framework and the tool exploiting a running example of a cholera outbreak.
Luca Bortolussi is an Associate Professor (since 2015) in Computer Science at the Department of Mathematics and Geosciences, University of Trieste and he is an associate researcher at ISTI-CNR in Pisa, Italy.
From June 2014 to May 2015, he was a guest professor at the department of Computer Science of the University of Saarland in Saarbruecken, Germany and previously an assistant professor of Computer Science at the Department of Mathematics and Geosciences of the University of Trieste, Italy. He graduated in Mathematics at the University of Trieste in 2003 and he got his PhD in Computer Science at the University of Udine in 2007. Until 2015, he was an honorary fellow of the School of Informatics of the University of Edinburgh, where he spent a sabbatical year in 2012. His research interests focus on quantitative formal methods, modelling and simulation and machine learning, with applications in computational biology and smart systems.
This talk is organized by the Cyber-Physical Systems Group at the Institute of Computer Engineering. It is a part of Erasmus Mundus Scholar within the European Master's Program in Computational Logic at TU Wien, Austria.