An STREL-based Formulation of Spatial Resilience in Cyber-Physical Systems
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917145083904000 |
|---|---|
| author | Zhang, Zeyu Chen, Hongkai Paoletti, Nicola Lin, Shan Smolka, Scott A. |
| author_facet | Zhang, Zeyu Chen, Hongkai Paoletti, Nicola Lin, Shan Smolka, Scott A. |
| contents | 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 $d_1, d_2$, the S-atom of $φ$, $S_{d_1, d_2} (φ)$, is the SREL formula $\negφR_{[0,d_1]} (φR_{[d_2, +\infty)}φ)$, specifying that recovery from a violation of $φ$ occurs within distance $d_1$ (recoverability), and subsequently that $φ$ 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}(φ)$ 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_12511 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | An STREL-based Formulation of Spatial Resilience in Cyber-Physical Systems Zhang, Zeyu Chen, Hongkai Paoletti, Nicola Lin, Shan Smolka, Scott A. Logic in Computer Science 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 $d_1, d_2$, the S-atom of $φ$, $S_{d_1, d_2} (φ)$, is the SREL formula $\negφR_{[0,d_1]} (φR_{[d_2, +\infty)}φ)$, specifying that recovery from a violation of $φ$ occurs within distance $d_1$ (recoverability), and subsequently that $φ$ 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}(φ)$ 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. |
| title | An STREL-based Formulation of Spatial Resilience in Cyber-Physical Systems |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2512.12511 |