Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An STREL-based Formulation of Spatial Resilience in Cyber-Physical Systems

Zeyu Zhang, Hongkai Chen, Nicola Paoletti, Shan Lin, Scott A. Smolka

TL;DR

This paper addresses the lack of a formal treatment for spatial resiliency in cyber-physical systems by extending the spatial fragment of STREL (SREL) into Spatial Resilience Specifications (SpaRS). It defines S-atoms $S_{d_1,d_2}()$ to capture recoverability within a distance and persistency along a route, and introduces Spatial Resilience Value (SpaRV) as a quantitative, non-dominated, Pareto-like set of recoverability-persistency pairs. An exact evaluation framework combines Dijkstra, DFS, and flooding-based methods to compute SpaRV and proves soundness and completeness with respect to SREL semantics. The approach is validated on two case studies—networked microgrids and a bike-sharing network—demonstrating the expressiveness and practical viability of spatial resilience reasoning in CPS. Overall, SpaRS provides a principled, multi-criteria formalism for reasoning about how CPS can recover from violations and sustain desired properties across space, with concrete algorithms and scalable case studies supporting real-world applicability.

Abstract

Resiliency is the ability of a system to quickly recover from a violation (recoverability) and avoid future violations for as long as possible (durability). In the spatial setting, recoverability and durability (now known as persistency) are measured in units of distance. Like its temporal counterpart, spatial resiliency is of fundamental importance for Cyber-Physical Systems (CPS) and yet, to date, there is no widely agreed-upon formal treatment of spatial resiliency. We present a formal framework for reasoning about spatial resiliency in CPS. Our framework is based on the spatial fragment of STREL, which we refer to as SREL. In this framework, spatial resiliency is given a syntactic characterization in the form of a Spatial Resiliency Specification (SpaRS). An atomic predicate of SpaRS is called an S-atom. Given an arbitrary SREL formula $\varphi$, distance bounds $d_1, d_2$, the S-atom of $\varphi$, $S_{d_1, d_2} (\varphi)$, is the SREL formula $\neg\varphi R_{[0,d_1]} (\varphi R_{[d_2, +\infty)}\varphi)$, specifying that recovery from a violation of $\varphi$ occurs within distance $d_1$ (recoverability), and subsequently that $\varphi$ be maintained along a route for a distance greater than $d_2$ (persistency). S-atoms can be combined using spatial STREL operators, allowing one to express composite resiliency specifications. We define a quantitative semantics for SpaRS in the form of a Spatial Resilience Value (SpaRV) function $σ$ and prove its soundness and completeness w.r.t. SREL's Boolean semantics. The $σ$-value for $S_{d_1,d_2}(\varphi)$ is a set of non-dominated (rec, per) pairs, quantifying recoverability and persistency, given that some routes may offer better recoverability while others better persistency. In addition, we design algorithms to evaluate SpaRV for SpaRS formulas. Finally, two case studies demonstrate the practical utility of our approach.

An STREL-based Formulation of Spatial Resilience in Cyber-Physical Systems

TL;DR

This paper addresses the lack of a formal treatment for spatial resiliency in cyber-physical systems by extending the spatial fragment of STREL (SREL) into Spatial Resilience Specifications (SpaRS). It defines S-atoms to capture recoverability within a distance and persistency along a route, and introduces Spatial Resilience Value (SpaRV) as a quantitative, non-dominated, Pareto-like set of recoverability-persistency pairs. An exact evaluation framework combines Dijkstra, DFS, and flooding-based methods to compute SpaRV and proves soundness and completeness with respect to SREL semantics. The approach is validated on two case studies—networked microgrids and a bike-sharing network—demonstrating the expressiveness and practical viability of spatial resilience reasoning in CPS. Overall, SpaRS provides a principled, multi-criteria formalism for reasoning about how CPS can recover from violations and sustain desired properties across space, with concrete algorithms and scalable case studies supporting real-world applicability.

Abstract

Resiliency is the ability of a system to quickly recover from a violation (recoverability) and avoid future violations for as long as possible (durability). In the spatial setting, recoverability and durability (now known as persistency) are measured in units of distance. Like its temporal counterpart, spatial resiliency is of fundamental importance for Cyber-Physical Systems (CPS) and yet, to date, there is no widely agreed-upon formal treatment of spatial resiliency. We present a formal framework for reasoning about spatial resiliency in CPS. Our framework is based on the spatial fragment of STREL, which we refer to as SREL. In this framework, spatial resiliency is given a syntactic characterization in the form of a Spatial Resiliency Specification (SpaRS). An atomic predicate of SpaRS is called an S-atom. Given an arbitrary SREL formula , distance bounds , the S-atom of , , is the SREL formula , specifying that recovery from a violation of occurs within distance (recoverability), and subsequently that be maintained along a route for a distance greater than (persistency). S-atoms can be combined using spatial STREL operators, allowing one to express composite resiliency specifications. We define a quantitative semantics for SpaRS in the form of a Spatial Resilience Value (SpaRV) function and prove its soundness and completeness w.r.t. SREL's Boolean semantics. The -value for is a set of non-dominated (rec, per) pairs, quantifying recoverability and persistency, given that some routes may offer better recoverability while others better persistency. In addition, we design algorithms to evaluate SpaRV for SpaRS formulas. Finally, two case studies demonstrate the practical utility of our approach.

Paper Structure

This paper contains 17 sections, 1 theorem, 11 equations, 3 figures, 1 table, 4 algorithms.

Table of Contents

  1. Introduction
  2. Our Contributions.
  3. Preliminaries
  4. A-Spatial Model
  5. Spatial Reach and Escape Logic (SREL)
  6. Specifying Spatial Resilience
  7. Spatial Resilience Specification (SpaRS) Language
  8. Evaluation Algorithm
  9. Evaluation of $S_{d_1,d_2}(\varphi)$
  10. Correctness.
  11. Complexity.
  12. Spatial operators
  13. Case studies
  14. Networked Microgrids
  15. Bike Sharing System
  16. ...and 2 more sections

Key Result

Theorem 3.10

Let $\xi$ be a spatial signal and $\psi$ a SpaRS specification. The following results at location $l$ hold: (1) $\exists x \in \sigma(\Sigma, \psi, \xi, l) \; s.t. \; x\mathrel{\succ_{\mathit{re}}} \mathbf{0} \Longrightarrow(\Sigma, \xi, l) \models \psi$ (2) $\exists x \in \sigma(\Sigma, \psi, \xi,

Figures (3)

  • Figure 1: Illustration of a solar power-driven rover and the corresponding spatial distribution of solar power. Locations satisfying the property $\varphi= \text{solar\_power}\geq1\text{kW}$ are shown as black nodes; white nodes indicate locations where the property does not hold.
  • Figure 2: In the NMG model, each node represents an individual microgrid, uniquely identified by a corresponding index.
  • Figure 3: In the graphs, each node represents a bike docking station, uniquely identified by a corresponding index.

Theorems & Definitions (19)

  • Example 1.1: Solar power-driven rover
  • Definition 2.1: A-spatial model 2022STREL
  • Definition 2.2: Route 2022STREL
  • Definition 2.3: Distance Domain 2022STREL
  • Definition 2.4: Distance functions and Route Length 2022STREL
  • Definition 2.5: Spatial signal
  • Definition 2.6: SREL syntax 2022STREL
  • Definition 2.7: SREL qualitative and quantitative semantics 2022STREL
  • Definition 3.1: Spatial Resiliency Specification (SpaRS)
  • Remark 3.2
  • ...and 9 more