Time-critical systems must satisfy temporal constraints whose correctness depends not only on event ordering but also on precise timing. Metric Interval Temporal Logic (MITL) provides a formalism to express such requirements. Although robustness has been widely studied under signal-based interpretations, it remains largely unexplored for point-based semantics, where executions are sequences of timestamped facts. In this setting, small timing variations may arbitrarily change Boolean satisfaction, revealing the instability of temporal truth under uncertainty. We introduce a notion of time robustness for MITL over point-based semantics, interpreting robustness as a margin of validity of temporal interpretations. We define a quantitative semantics and prove soundness with respect to Boolean satisfaction together with a Lipschitz stability property with respect to timestamp perturbations, which induces a metric notion of proximity between interpretations. The semantics admits a polynomial-time evaluation procedure and is illustrated on two case studies (drone surveillance and smart hospital), where robustness empirically correlates with tolerance to temporal noise.

Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the spatial configuration of the various components and agents. In these settings, robust monitoring of the distributed components is vital to ensuring complex behaviors are achieved, and safety properties are maintained. To this end, we look at defining the automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic designed to express and monitor spatio-temporal requirements over mobile, spatially distributed CPS. Specifically, STREL reasons about spatio-temporal behavior over dynamic weighted graphs. While STREL is endowed with well defined qualitative and quantitative semantics, in this paper, we propose a novel construction of (weighted) alternating finite automata from STREL specifications that efficiently encodes these semantics. Moreover, we demonstrate how this automaton semantics can be used to perform both, offline and online monitoring for STREL specifications using a simulated drone swarm environment.

Describing the properties of complex systems that evolve over time is a crucial requirement for monitoring and understanding them. Signal Temporal Logic (STL) is a framework that proved to be effective for this aim because it is expressive and allows state properties as human-readable formulae. Crafting STL formulae that fit a particular system is, however, a difficult task. For this reason, a few approaches have been proposed recently for the automatic learning of STL formulae starting from observations of the system. In this paper, we propose BUSTLE (Bi-level Universal STL Evolver), an approach based on evolutionary computation for learning STL formulae from data. BUSTLE advances the state of the art because it (i) applies to a broader class of problems, in terms of what is known about the state of the system during its observation, and (ii) generates both the structure and the values of the parameters of the formulae employing a bi-level search mechanism (global for the structure, local for the parameters). We consider two cases where (a) observations of the system in both anomalous and regular state are available, or (b) only observations of regular state are available. We experimentally evaluate BUSTLE on problem instances corresponding to the two cases and compare it against previous approaches. We show that the evolved STL formulae are effective and human-readable: the versatility of BUSTLE does not come at the cost of lower effectiveness.

Application development for the modern web involves sophisticated engineering workflows—including user interface (UI) aspects. Such user interfaces comprise web elements that are typically created with HTML/CSS markup and JavaScript-like languages, yielding web documents. Their testing entails performing checks to examine visual and structural parts of the resulting UI software against requirements such as usability, accessibility, performance, or, increasingly, compliance with standards. However, current techniques are largely ad hoc and tailor-made to specific classes of requirements or web technologies and extensively require human-in-the-loop qualitative evaluations. Web UI evaluation so far has lacked formal foundations, which would provide assurances of compliance with requirements in an automatic manner. To this end, we devise a methodology and accompanying technical framework for web UIs. In our approach, requirements are formally specified in a spatio-temporal logic able to capture both the layout of visual components as well as how they change over time, as a user interacts with them. The technique we advocate is independent of the underlying technologies a web application may be developed with, as well as the browser and operating system used. To concretely support the specification and evaluation of UI requirements, our framework is grounded on open source tools for instrumenting, analyzing, and reporting spatio-temporal behaviors in webpages. We demonstrate our approach in practice over web accessibility standards posing challenges for automated verification.

Integrating symbolic knowledge and data-driven learning algorithms is a longstanding challenge in Artificial Intelligence. Despite the recognized importance of this task, a notable gap exists due to the discreteness of symbolic representations and the continuous nature of machine-learning computations. One of the desired bridges between these two worlds would be to define semantically grounded vector representation (feature embedding) of logic formulae, thus enabling to perform continuous learning and optimization in the semantic space of formulae. We tackle this goal for knowledge expressed in Signal Temporal Logic (STL) and devise a method to compute continuous embeddings of formulae with several desirable properties: the embedding (i) is finite-dimensional, (ii) faithfully reflects the semantics of the formulae, (iii) does not require any learning but instead is defined from basic principles, (iv) is interpretable. Another significant contribution lies in demonstrating the efficacy of the approach in two tasks: learning model checking, where we predict the probability of requirements being satisfied in stochastic processes; and integrating the embeddings into a neuro-symbolic framework, to constrain the output of a deep-learning generative model to comply to a given logical specification.

Abstract We present MoonLight, a tool for monitoring temporal and spatio-temporal properties of mobile, spatially distributed, and interacting entities such as biological and cyber-physical systems. In MoonLight the space is represented as a weighted graph describing the topological configuration in which the single entities are arranged. Both nodes and edges have attributes modeling physical quantities and logical states of the system evolving 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, such as Java API, or via Matlab™ and Python interfaces. We provide here the description of the tool, its interfaces, and its scripting language using a sensor network and a bike sharing example. We evaluate the tool performances both by comparing it with other tools specialized in monitoring only temporal properties and by monitoring spatio-temporal requirements considering different sizes of dynamical and spatial graphs.

Application development for the modern Web involves sophisticated engineering workflows which include user interface aspects. Those involve Web elements typically created with HTML/CSS markup and JavaScript-like languages, yielding Web documents. WebMonitor leverages requirements formally specified in a logic able to capture both the layout of visual components as well as how they change over time, as a user interacts with them. Then, requirements are verified upon arbitrary web pages, allowing for automated support for a wide set of use cases in interaction testing and simulation. We position WebMonitor within a developer workflow, where in case of a negative result, a visual counterexample is returned. The monitoring framework we present follows a black-box approach, and as such is independent of the underlying technologies a Web application may be developed with, as well as the browser and operating system used.

Abstract We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of akernel function, well known in machine learning as a conceptually and computationally efficient tool. The correspondingkernel trickallows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task ofpredicting (quantitative) satisfactionof STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor.

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.

From biological systems to cyber-physical systems, monitoring the behavior of such dynamical systems often requires reasoning about complex spatio-temporal properties of physical and 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 reason about spatio-temporal properties. STREL considers each system's entity as a node of a dynamic weighted graph representing its spatial arrangement. Each node generates a set of mixed-analog signals describing the evolution over time of computational and physical quantities characterizing 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.

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. Comment: 36 pages with 13 figures

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, the spatial and temporal requirements play an essential role for their correct and safe execution. Furthermore, the local interactions among the system components result in global spatio-temporal emergent behaviors often impossible to predict at the design time. In this work, we pursue a complementary approach by introducing STREL a novel spatio-temporal logic that enables the specification of spatio-temporal requirements and their monitoring over the execution of mobile and spatially distributed CPS. Our logic extends the Signal Temporal Logic [15]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 neighbours, 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 optimisation. We prove that, for a subclass of models, all the spatial properties expressed with reach and escape, using euclidean distance, satisfy all the model transformations using rotation, reflection and translation. Finally, we provide an offline monitoring algorithm for STREL and, to demonstrate the feasibility of our approach, we show its application using the monitoring of a simulated mobile ad-hoc sensor network as running example.