SpaTeL: A Novel Spatio-Temporal Logic and its Applications to Networked Systems

Networked dynamical systems are increasingly used as models for a variety of processes ranging from robotic teams to collections of genetically engineered living cells.  As the complexity of these systems increases, so does the range of emergent properties that they exhibit.  In this work, we define a new logic called Spatio-Temporal Logic (SpaTeL) that is a unification of signal temporal logic (STL) and tree spatial superposition logic (TSSL).  SpaTeL is capable of describing high-level spatial patterns that change over time, e.g. "Power consumption in the northwest quadrant of the city drops below 100 megawatts if the power consumption in the southwest quadrant remains above 200 megawatts for two hours."  We present a statistical model checking procedure that evaluates the probability with which a networked system satisfies a SpaTeL formula.  We also develop a synthesis procedure that determines system parameters maximizing the average degree of satisfaction, a continuous measure that quantifies how strongly a system execution satisfies a given formula.  We demonstrate our algorithms on two systems: a biochemical reaction-diffusion system and a demand-side management system for a smart neighbourhood.

Bio: I am currently a tenure-track Assistant Professor (holding the National Habilitation as Associate Professor in Italy) at the Faculty of Informatics, Cyber-Physical Systems Group at the Vienna University of Technology.  The primary focus of my research is to develop formal methods, tools and techniques which support the modeling and the automated analysis of complex computational systems, including software systems, embedded systems and biological systems.  On these topics I was the author or coauthor of more than 50 papers published in refereed journals, edited books, and refereed conference proceedings.

I joined the Faculty of Informatics in 2012 as a University Assistant at Vienna University of Technology.  I recently won a "Laufbahnstelle," becoming a tenure-track Assistant Professor.  Previously I was a post-doctoral researcher at the Department of Computer Science (Research Scientist - from March 2011) and at the Department of Applied Math and Statistics (Research Associate - from February 2010) of the State University of New York at Stony Brook, working with Prof James Glimm, Prof Radu Grosu and Prof Scott A. Smolka.  My research area, in the framework of the NSF Expeditions in Computing project CMACS, was the Computational Modelling and Analysis of Cardiac Dynamics for Prediction and Control of Cardiac Arrhythmia.  I received the BS degree in Computer Science and the MS degree in Bioinformatics from the University of Camerino in Italy, in 2002 and 2005 respectively.  In 2009 I got a PhD in Complex Systems and Information Sciences from the University of Camerino.  In 2014 I earned the National Italian Habilitation as Associate Professor in Computer Science by the Italian Ministry of Education, Universities and Research.

I co-chaired several international events, such as HSB 2012, the First International Workshop on Hybrid Systems and Biology, SPIN 2013, the 20th International Symposium on Model Checking Software, the CSRV-2014, the First International Competition of Software Runtime Verification in Canada, the Medial CPS track at Isola 2014.  In 2015 I will co-chair in Vienna the 15th International Conference on Runtime Verification and in 2016 I will be one of the organisers and the local accommodation Chair of the CPS week in Vienna.  I also serve as Editorial Board Member of the International Journal of Information and Computation (Elsevier).  I represent Austria in the management committee of the EU COST ICT action ARVI on Runtime Verification and I co-chair the RV core working group in this action.