Runtime Monitoring of Real time Safety Requirements in Smart Cities
There is an increasing need for the runtime monitoring of real time safety and performance requirements in smart cities. In this paper, we present SaSTL, a novel Spatial Aggregation Signal Temporal Logic, to specify and monitor real time requirements in smart cities. We also develop an efficient runtime monitoring algorithm that can check in parallel a SaSTL requirement over multiple data streams generated from thousands of sensors that are typically spatially distributed over a smart city. We evaluate the real time SaSTL monitor by applying it to two city application scenarios with large scale real sensing data, (e.g., up to 10,000 sensors in one requirement). The results show that SaSTL monitoring can help improve the city performance in simulated experiments (e.g., 21.1% on the environment and 16.6% on public safety) with a significant reduction of computation time compared with previous approaches (e.g., from 2 hours to 30 minutes on average when monitoring 80 requirements).
Spatial Temporal Logic Verification, and Synthesis
Networked dynamical systems are increasingly used as models for a variety of processes ranging from robotic teams to collections of genetically engineered living cells and power networks. As the complexity of these systems increases, so does the range of emergent properties that they exhibit. In this talk, I will focus on a logic called Spatial-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.” I will present a statistical model checking procedure that evaluates the probability with which a networked system satisfies a SpaTeL formula. I will also demonstrate 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. I will illustrate the approach on three systems: a biochemical reaction-diffusion system, a human pluripotent stem system, and a demand-side management system for a smart neighborhood.
A novel logic for analyzing the spatio-temporal properties of spatial stochastic systems
We consider systems in which dynamic behaviour is spatially distributed and also stochastic. In particular the agents within the system have a location, and the ability of agents to interact may depend on agents being co-located or within a given range of each other. Such systems are typically studied by simulations. Current simulation-based approaches provide summary information about the satisfaction of properties over the spatial domain, providing estimated values that include intrinsic uncertainty. In this work we seek to take this uncertainty into account and to enrich the summary information through the use of a novel logic, the Three-Valued Spatio-Temporal Logic (TSTL), which allows us to reason, not only about the behaviour of the system, but also about the evolution of the satisfaction of properties expressed in a spatio-temporal logic. This provides additional insight into the dynamic behaviour of the system under study. For example, in the analysis of the efficacy of a control measure for fire spread, we can verify whether the spread in a specific area will happen with probability under a given threshold over time. We can also identify the locations that are at highest risk, because they are surrounded by locations with high probability of burning. We use a three-valued logic, with the third value unknown indicating when there is insufficient evidence to make a judgement about a property. This can be taken as an indication of when more simulation trajectories are needed to evaluate propositions more precisely.
Especially for the verification of cyber-physical systems, one has to reason about their location over time to ensure their safe operation. While static verification may seem preferable in many cases, the complexity of such techniques limit their application. At the same time, runtime verification checking the execution of the underlying system is getting more and more attention.
In this work we introduce a mechanism for synthesis of monitors suitable for runtime verification using a decision procedure for the unification of the temporal logic LTL and BRCC-8. BRCC-8 is a spatial logic with pedigree on region calculus. Our solution is based on the application of modern SMT solvers to prove or refute the properties we want to verify and also on the implementation of the notion of metric spaces well known in topology. This work is also inspired on monitoring modulo theories.
Target Counting with Wireless Sensor Networks: Spatio-Temporal Models and Presburger Arithmetic
One of the applications popularised by the emergence of wireless sensor networks is target counting: the computational task of determining the total number of targets located in an area by aggregating the individual counts of each sensor. The complexity of this task lies in the fact that sensing ranges may overlap, therefore targets may be overcounted as, in this setting, they are assumed to be indistinguishable from each other. In the literature, this problem has been proven to be unsolvable, hence the existence of several estimation algorithms. However, the main limitation currently affecting these algorithms is that no assurance regarding the precision of a solution can be given. In this talk, I present a formal model developed to reason about topologies created by sensor ranges, and a first-order logic tailored to specify relations between parts of the space with respect to sensor coverage. Furthermore, sketch how the model can be extended to take mobile sensors and temporal aspects into account. Subsequently, I present a novel algorithm for target counting based on exhaustive enumeration of target distributions using linear Presburger constraints. This algorithm improves on current approaches since the obtained estimated counts are by construction guaranteed to be consistent with the counts of each sensor, and can be extended to allow for weighted topologies and sensing errors.
Monitoring Mobile and SpatiallyDistributed Cyber-Physical Systems
Cyber-Physical Systems (CPS) consist of collaborative, networked and tightly intertwined computational (logical) and physical components, each operating at different spatial and temporal scales. Hence, spatial along with the temporal requirements play an essential role in their correct and safe execution. However, the local interactions among the system components result in global Spatio-temporal emergent behaviors often impossible to predict at the design time. In this talk, we introduce a novel Spatio-temporal logic that enables the specification of Spatio-temporal requirements and to monitor them over the execution of mobile and spatially distributedCPS. The logic extends the Signal Temporal Logic with two novel spatial operators reach and escape from which is possible to derive other spatial modalities such as everywhere, somewhere and surround. These operators enable a monitoring procedure where the satisfaction of the property at each location depends only on the satisfaction of its neighbors, opening the way to future distributed online monitoring algorithms. We propose both a qualitative and quantitative semantics-based on constraint semirings, an algebraic structure suitable for constraint satisfaction and optimization.
Counting Temporal Logics for Multi-Agent Planning and Beyond
Many robotic swarm or Internet-of-Things applications require coordinating a large collection of agents. In these problems, often times, identities of individual agents are not important for the collection to achieve its overall goal. In this talk I will introduce two logics designed for specifying correct behavior in this multi-agent setting: counting linear temporal logic (cLTL) and counting linear temporal logic plus (cLTL+). These logics provide a way to compactly specify spatial-temporal constraints by exploiting the permutation invariance of the tasks with respect to agents. I will discuss some properties of these logics and corresponding algorithms for scalable control design. Finally, I will demonstrate the approach on several problems including multi-robot emergency response and coordination of thermostatically controlled loads in smart grids.
Dynamic Cyber-Physical Spaces
Computing and communication capabilities are increasingly being embedded into physical spaces blurring the boundary between computational and physical worlds; typically, this is the case in modern cyber-physical or internet-of-things (IoT) systems. Conceptually, such composite environments can be abstracted into a topological model where computational and physical entities are connected in a graph structure, yielding a cyber-physical space. Like any other software-intensive system, such a space is highly dynamic and typically undergoes continuous change – it is evolving. This brings a manifold of challenges as dynamics may affect e.g. safety, security, or reliability requirements. Modelling space and its dynamics as well as supporting formal reasoning about various properties of an evolving space, are crucial prerequisites for engineering dependable space-intensive systems, e.g. to assure requirements satisfaction or to trigger correct adaptation.
This talk will show an avenue for research which can be characterized as rethinking spatial environments from a software engineering perspective — in both design and operation aspects. Regarding design, we will see how domain descriptions can give rise to models amenable to automated analyses of dynamic behaviours on spaces populated with humans, robots, or mobile devices. Analysis amounts to assessing if some collective behaviour that is highly space-dependent, violates certain requirements that the overall system should exhibit. Regarding runtime, we will consider supporting analyses on the cloud on behalf of resource-constrained and spatially-distributed IoT devices. We will discuss how spatial verification processes can be integrated in the service layer of an IoT-cloud architecture based on microservices, and what tradeoffs emerge across different deployment options.
Guiding motion with signal temporal logic
The increasing number of emerging autonomous robotics application bring the increasing need to cope with advanced objectives and requirements regarding the robots’ interaction with their environment and each other. In this talk, we focus on motion planning with spatio-temporal preferences. Motion planning is traditionally posed as finding a collision-free trajectory from an initial state to a goal state. However, recently proposed motion planning with temporal logic specifications allows to treat more involved planning objectives, such as periodic surveillance, sequencing, or request-response tasks, as well as various motion constraints and preferences. We show how to couple quantitative semantics – robustness – of Signal Temporal Logic (STL) with a sampling-based motion planning algorithm RRT* in order to keep robots within desired distances from obstacles, points of interest, and each other in a maximally satisfying way. Finally, we demonstrate an impact of guiding motion planning with STL on exploration with Unmanned Aerial Vehicles (UAVs) in experiments.