A logic-based approach to specify and design spatio-temporal behaviours of complex systems

Models of complex systems, composed of many heterogeneous interacting components, are challenging to analyse, due to the size and complexity of the network of interactions among the individual entities. The analysis becomes even more challenging when the spatio-temporal aspects of the system are to be taken into account. In this thesis, we propose a framework of efficient techniques to validate and analyse the behaviour of complex systems with spatio-temporal dynamics, both in the stochastic and deterministic cases. In particular, we define Signal Spatio-Temporal Logic (SSTL), a spatial extension of Signal Temporal Logic (STL). SSTL presents two new operators: the bounded somewhere and the bounded surround, that can be used to specify metric and topological properties in a discrete space. Given an SSTL formula, we design efficient monitoring algorithms to check its validity and compute its satisfaction (robustness) score over a spatio-temporal trace. To deal with stochastic systems, we define a stochastic version of the quantitative semantics of STL that we extended later to SSTL. We then combine it with machine learning techniques to define efficient parameter estimation and system design procedures. The specification and validation of SSTL formulae have been implemented in a Java tool, jSSTL. Finally, the expressivity of SSTL and the efficiency of the algorithms developed in this work are showed on interested and challenging case studies, including an epidemic spreading model of a waterborne disease, a pattern formation example for reaction-diffusion systems and a french flag model of the morphogen Bicoid