This workshop aims to present the most recent advances in the development of logic-based procedures for the analysis and control of spatially distributed Cyber Physical Systems (CPS), with particular emphasis on the combination of temporal and spatial behaviors. Spatially distributed CPS, such as robotic swarms and smart environments, often exhibit multiple and unpredictable behaviors that increase the efforts needed in their analysis. Studying and controlling such systems requires a growing demand for efficient tools capable of dealing with such complex behavioral patterns. (Spatio)-temporal logic is an innovative way to reason and face such challenges.

This workshop has the dual objective:

1) showing the usefulness of (spatio)-temporal logic to the control community in the context of spatially distributed CPS and

2) highlighting what are the main important challenges in the analysis of such systems that the logic community can help to solve in the near future. Several case studies will be considered to discuss the real usefulness of these methodologies. This will lay the foundations for a verification framework of spatially distributed CPS as well as fill the gap between theory and practice of CPS design, deployment, and testing, with particular emphasis on the decision procedures and monitoring mechanisms.

Target Audience

The workshop aims to attract PhD students and researchers with a common interest in the verification and control of spatially-distributed CPS, as well as to expose them to the state-of the art and the current challenges in the field of spatio-temporal logics. We mainly expect participants from formal methods and control community but participants from other disciplines can also join, since one of the main objectives of the workshop is to share and discuss the applicability of the spatio-temporal reasoning on the field of control systems and all talks will be self-contained, including the necessary background.