Monitoring Spatially Distributed Cyber-Physical Systems with Alternating Finite Automata
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915217500274688 |
|---|---|
| author | Balakrishnan, Anand Paul, Sheryl Silvetti, Simone Nenzi, Laura Deshmukh, Jyotirmoy V. |
| author_facet | Balakrishnan, Anand Paul, Sheryl Silvetti, Simone Nenzi, Laura Deshmukh, Jyotirmoy V. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_21906 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Monitoring Spatially Distributed Cyber-Physical Systems with Alternating Finite Automata Balakrishnan, Anand Paul, Sheryl Silvetti, Simone Nenzi, Laura Deshmukh, Jyotirmoy V. Logic in Computer Science Formal Languages and Automata Theory Multiagent Systems 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. |
| title | Monitoring Spatially Distributed Cyber-Physical Systems with Alternating Finite Automata |
| topic | Logic in Computer Science Formal Languages and Automata Theory Multiagent Systems |
| url | https://arxiv.org/abs/2503.21906 |