Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userQualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTL
156
0
0.0
(
0
)
Added by
Christoph Rauch
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
In spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which efficient monitoring algorithms have been developed. As such, it is suitable for real-time verification of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satisfies a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diffusion system and spatio-temporal aspects of a large bike-sharing system.
rate research
Read More
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 systems 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 nodes 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 systems 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 systems behavior with its specification. Finally, we demonstrate our approach in a real-world environmental monitoring case study.
We present MoonLight, a tool for monitoring temporal and spatio-temporal properties of mobile and spatially distributed cyber-physical systems (CPS). In the proposed framework, space is represented as a weighted graph, describing the topological configurations in which the single CPS entities (nodes of the graph) are arranged. Both nodes and edges have attributes modelling physical and logical quantities that can change in time. MoonLight is implemented in Java and supports the monitoring of Spatio-Temporal Reach and Escape Logic (STREL). MoonLight can be used as a standalone command line tool, as a Java API, or via Matlab interface. We provide here some examples using the Matlab interface and we evaluate the tool performance also by comparing with other tools specialized in monitoring only temporal properties.
We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a finite-state program, executed by an unknown number of indistinguishable agents, where the next agent to make a move is determined by the result of a random experiment. We show that if a property of such a system holds, then there is always a witness in the shape of a Presburger stage graph: a finite graph whose nodes are Presburger-definable sets of configurations. Due to the high complexity of the verification problem (non-elementary), we introduce an incomplete procedure for the construction of Presburger stage graphs, and implement it on top of an SMT solver. The procedure makes extensive use of the theory of well-quasi-orders, and of the structural theory of Petri nets and vector addition systems. We apply our results to a set of benchmarks, in particular to a large collection of population protocols, a model of distributed computation extensively studied by the distributed computing community.
To make progress in understanding the issue of memory loss and history dependence in evolving complex systems, we consider the mixing rate that specifies how fast the future states become independent of the initial condition. We propose a simple measure for assessing the mixing rate that can be directly applied to experimental data observed in any metric space $X$. For a compact phase space $X subset R^M$, we prove the following statement. If the underlying dynamical system has a unique physical measure and its dynamics is strongly mixing with respect to this measure, then our method provides an upper bound of the mixing rate. We employ our method to analyze memory loss for the system of slowly sheared granular particles with a small inertial number $I$. The shear is induced by the moving walls as well as by the linear motion of the support surface that ensures approximately linear shear throughout the sample. We show that even if $I$ is kept fixed, the rate of memory loss (considered at the time scale given by the inverse shear rate) depends erratically on the shear rate. Our study suggests a presence of bifurcations at which the rate of memory loss increases with the shear rate while it decreases away from these points. We also find that the memory loss is not a smooth process. Its rate is closely related to frequency of the sudden transitions of the force network. The loss of memory, quantified by observing evolution of force networks, is found to be correlated with the loss of correlation of shear stress measured on the system scale. Thus, we have established a direct link between the evolution of force networks and macroscopic properties of the considered system.
The activity of a sparse network of leaky integrate-and-fire neurons is carefully revisited with reference to a regime of a bona-fide asynchronous dynamics. The study is preceded by a finite-size scaling analysis, carried out to identify a setup where collective synchronization is negligible. The comparison between quenched and annealed networks reveals the emergence of substantial differences when the coupling strength is increased, via a scenario somehow reminiscent of a phase transition. For sufficiently strong synaptic coupling, quenched networks exhibit a highly bursting neural activity, well reproduced by a self-consistent approach, based on the assumption that the input synaptic current is the superposition of independent renewal processes. The distribution of interspike intervals turns out to be relatively long-tailed; a crucial feature required for the self-sustainment of the bursting activity in a regime where neurons operate on average (much) below threshold. A semi-quantitative analogy with Ornstein-Uhlenbeck processes helps validating this interpretation. Finally, an alternative explanation in terms of Poisson processes is offered under the additional assumption of mutual correlations among excitatory and inhibitory spikes.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
