Search

Cyber-Physical Systems (CPS) consist of inter-wined computational (cyber) and physical components interacting through sensors and/or actuators. Computational elements are networked at every scale and can communicate with each other and with humans. Nodes can join and leave the network at any time or they can move to different spatial locations. In this scenario, monitoring spatial and temporal properties plays a key role in the understanding of how complex behaviors can emerge from local and dynamic interactions. We revisit here the Spatio-Temporal Reach and Escape Logic (STREL), a logic-based formal language designed to express and monitor spatio-temporal requirements over the execution of mobile and spatially distributed CPS. STREL considers the physical space in which CPS entities (nodes of the graph) are arranged as a weighted graph representing their dynamic topological configuration. Both nodes and edges include attributes modeling physical and logical quantities that can evolve over time. STREL combines the Signal Temporal Logic with two spatial modalities reach and escape that operate over the weighted graph. From these basic operators, we can derive other important spatial modalities such as everywhere, somewhere and surround. We propose both qualitative and quantitative semantics based on constraint semiring algebraic structure. We provide an offline monitoring algorithm for STREL and we show the feasibility of our approach with the application to two case studies: monitoring spatio-temporal requirements over a simulated mobile ad-hoc sensor network and a simulated epidemic spreading model for COVID19., Comment: arXiv admin note: substantial text overlap with arXiv:1904.08847

This deliverable is an account of the QUANTICOL software tool suite, with application to the smart city scenarios studied in the project. While Deliverable D4.3 focuses on the CARMA language and its implementation with the CARMA Eclipse plug-in, in this deliverable we present software tools developed to support further techniques such as model checking, model order reduction, and reachability analysis. Their integration with the CARMA Eclipse plug-in is discussed in Deliverable D4.3. Instead, here we provide detailed account of such tools as stand-alone products. We present FlyFast, a probabilistic model checker for mean-field models; jSSTL, for the analysis of Signal Spatio-Temporal Logic; ERODE, for the reduction of systems of ordinary differential equations; UTOPIC, for the reachability analysis of nonlinear dynamical systems; and topochecker, a spatio-temporal model checker. While an application of FlyFast to smart cities is presented in D4.3, in this deliverable we discuss an application of jSSTL and ERODE to the verification and reduction, respectively, of a model of a bike-sharing system. Instead, bus transportation systems are studied with topochecker, to detect problems in vehicle location data and clumping in frequent services.

This Internal Report describes the status of the work performed in the project on the extension of the theoretical foundations of scalable model-checking approaches with suitable notions of spatial verification. Various forms of scalable model-checking were developed during the first phase of Task 3.1 of WP3, including those based on mean-field and fluid flow techniques, and were presented in Deliverable 3.1. The focus of the present report is on forms of spatial verification based on model-checking techniques in which the effect of inhomogeneous spatial distribution of objects is taken into account. Several spatial logics have been developed and explored. The Spatial Logic for Closure Spaces (SLCS) is based on the formal framework of closure spaces. The latter include topological spaces but also discrete spaces such as graphs and therefore form a promising candidate for a uniform framework to develop spatial logics that can be applied to the various spatial representations presented in the deliverables of WP2. Closure spaces come with a well-developed theory and some powerful operators that turned out to be very useful both for the definition of the semantics of SLCS and for the development of spatial and spatio-temporal modelchecking algorithms. The spatial operators of SLCS have been also added to the Signal Temporal Logic (STL) to obtain Spatial Signal Temporal Logic (SSTL). In this case the spatial operators have been extended with spatial bounds based on distance measures and a quantitative semantics has been provided that is used to evaluate the robustness of the spatio-temporal formulas for signals. Spatial and spatio-temporal performance analysis measures have been explored for a simple PALOMA model of a group of robots and for a bike sharing model based on Markov Renewal Processes. The latter provides a simulation model of bike-sharing systems that includes users as agents. It also generates simulation traces with spatio-temporal information on bike stations that can be analysed using the prototype spatiotemporal model checkers that have been developed in the context of the project. A partial-differential approximation has been developed for spatial stochastic process algebra. The approach is validated on the well-known Lotka-Volterra model and shows an advantage in terms of computational efficiency compared to traditional numerical solutions. Finally, for what concerns scalable verification, the innovative model-checking approaches based on fluid approximation and on-the-fly mean-field techniques have been finalised. For the latter a prototype modelchecker, FlyFast, has been made available, which was described in Deliverable 5.2. QUANTICOL

We address the specification and verification of spatio-temporal behaviours of complex systems, extending Signal Spatio-Temporal Logic (SSTL) with a spatial operator capable of specifying topological properties in a discrete space. The latter is modelled as a weighted graph, and provided with a boolean and a quantitative semantics. Furthermore, we define efficient monitoring algorithms for both the boolean and the quantitative semantics. These are implemented in a Java tool available online. We illustrate the expressiveness of SSTL and the effectiveness of the monitoring procedures on the formation of patterns in a Turing reaction-diffusion system. Keywords: Signal Spatio-Temporal Logic, Boolean Semantics, Quantitative Semantics, Monitoring Algorithms, Weighted Graphs, Turing Patterns.

Space is important in the QUANTICOL project because the project case studies include smart transport, and quantitative modelling of transport has inherent spatial aspects. This deliverable presents a review of the literature about spatial modelling within and beyond computer science, and a classification of the different approaches reviewed. The objective of the classification is to make clear what approaches are available and how they differ from each other. This will be used to guide future work on spatial approaches within the project. Furthermore, the classification enables the identification of the approaches that have been used in the initial work on case studies in the realm of smart transport. This deliverable rst identifies the aspects of non-spatial modelling that are important in the context of the QUANTICOL project. Time can be modelled in a discrete or continuous manner. States can be discrete, representing attributes of an individual. For example, when considering bike sharing, inUse (busy), onStand (idle) or atWorkshop (under repair) might be appropriate states for a bike. Alternatively, states can be continuous representing an attribute (for example, seat height). In the case of discrete states, it is possible to perform aggregation by considering populations, namely how many individuals are in each state, and to acquire an understanding of the overall behaviour of the population, rather than of individuals. Mean-field techniques can be employed to transform a discrete population approach to one that considers continuous populations that approximate the discrete approach. To this context, space is introduced. Space can be discrete and described by a graph of locations. Depending on the structure of the graph and the parameters associated with locations and movement between locations, discrete space can be classified as regular or homogeneous. Space can be seen as continuous: as Euclidean space in one, two or three dimensions. Space can also be considered abstractly as topological space, whether discrete or continuous and this approach allows for reasoning about concepts such as adjacency and neighbourhoods. This deliverable describes the modelling techniques that are currently available for the different combinations of time, state, aggregation and space, giving both a tabular classification as well as high-level and formal descriptions of the techniques. For each representation, examples are given of its use in different disciplines, including ecology, biology, epidemiology and computer science. In particular, the modelling goals are considered for these techniques, and compared with the goals of the QUANTICOL project. This deliverable also has the aim of identifying disparate uses of terminology in various approaches. Both current and future case studies relevant to the project are classified in terms of how they use time, state, aggregation and space and nally conclusions are presented taking into account the literature reviewed, what has been modelled and what the goals of the project are for modelling of smart transport. The preliminary guidelines arising from the review and classification are to focus on patch models and associated techniques although continuous space models of individuals may be important in certain cases. Items proposed for further research are understanding and developing mean-field techniques, spatial and non-spatial moment closure methods and hybrid spatial approaches. The document closes with a future work plan for Work Package 2.

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires to reason about complex spatio-temporal properties of physical and/or computational entities that are dynamically interconnected and arranged in a particular spatial configuration. Spatio-Temporal Reach and Escape Logic (STREL) is a recent logic-based formal language designed to specify and to reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing their spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterising the node's behavior. While there are offline algorithms available for monitoring STREL specifications over logged simulation traces, here we investigate for the first time an online algorithm enabling the runtime verification during the system's execution or simulation. Our approach extends the original framework by considering imprecise signals and by enhancing the logics' semantics with the possibility to express partial guarantees about the conformance of the system's behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.

The Internet-of-Things, complex sensor networks, multi-agent cyber-physical systems are all examples of spatially distributed systems that continuously evolve in time. Such systems generate huge amounts of spatio-temporal data, and system designers are often interested in analyzing and discovering structure within the data. There has been considerable interest in learning causal and logical properties of temporal data using logics such as Signal Temporal Logic (STL); however, there is limited work on discovering such relations on spatio-temporal data. We propose the first set of algorithms for unsupervised learning for spatio-temporal data. Our method does automatic feature extraction from the spatio-temporal data by projecting it onto the parameter space of a parametric spatio-temporal reach and escape logic (PSTREL). We propose an agglomerative hierarchical clustering technique that guarantees that each cluster satisfies a distinct STREL formula. We show that our method generates STREL formulas of bounded description complexity using a novel decision-tree approach which generalizes previous unsupervised learning techniques for Signal Temporal Logic. We demonstrate the effectiveness of our approach on case studies from diverse domains such as urban transportation, epidemiology, green infrastructure, and air quality monitoring.

From the formation of traffic jams to the development of troublesome, whirlpool-like spirals in the heart’s electrical activity, spatio-temporal patterns are key in understanding how complex behaviors can emerge in a network of locally interacting dynamical systems. One of the most important and intriguing questions is how to specify spatio-temporal behaviors in a formal and human-understandable specification language and how to monitor their onset efficiently. In this tutorial, we present the spatio-temporal logic STREL and its expressivity to specify and monitor spatio-temporal behaviors over complex dynamical and spatially distributed systems. We demonstrate our formalism’s applicability to different scenarios considering static or dynamic spatial configurations and systems with deterministic or stochastic dynamics.

International audience; From smart buildings to medical devices to smart nations, software systems increasingly integrate computation, networking, and interaction with the physical environment. These systems are known as Cyber-Physical Systems (CPS). While these systems open new opportunities to deliver improved quality of life for people and reinvigorate computing, their engineering is a difficult problem given the level of heterogeneity and dynamism they exhibit. While progress has been made, we argue that complexity is now at a level such that existing approaches need a major rethink to define principles and associated techniques for CPS. In this paper, we identify research challenges when modelling, analysing and engineering CPS. We focus on three key topics: theoretical foundations of CPS, self-adaptation methods for CPS, and exemplars of CPS serving as a research vehicle shared by a larger community. For each topic, we present an overview and suggest future research directions, thereby focusing on selected challenges. This paper is one of the results of the Shonan Seminar 118 on Modelling and Analysing Resilient Cyber-Physical Systems, which took place in December 2018.

In this article, we present Three-Valued spatio-temporal Logic (TSTL), which enriches the available spatiotemporal analysis of properties expressed in Signal spatio-temporal Logic (SSTL), to give further insight into the dynamic behavior of systems. Our novel analysis starts from the estimation of satisfaction probabilities of given SSTL properties and allows the analysis of their temporal and spatial evolution. Moreover, in our verification procedure, we use a three-valued approach to include the intrinsic and unavoidable uncertainty related to the simulation-based statistical evaluation of the estimates; this can be also used to assess the appropriate number of simulations to use depending on the analysis needs. We present the syntax and three-valued semantics of TSTL and specific extended monitoring algorithms to check the validity of TSTL formulas. We introduce a reliability requirement for TSTL monitoring and an automatic procedure to verify it. Two case studies demonstrate how TSTL broadens the application of spatio-temporal logics in realistic scenarios, enabling analysis of threat monitoring and privacy preservation based on spatial stochastic population models.