Multi-Fidelity Temporal Reasoning: A Stratified Logic for Cross-Scale System Specifications
We present <b>S</b>tratified <b>M</b>etric <b>T</b>emporal <b>L</b>ogic (SMTL), a novel formalism for specifying and verifying the properties of complex cyber–physical systems that exhibit behaviors across multiple temporal and abstraction scales. SMTL...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2025-06-01
|
| Series: | Logics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2813-0405/3/2/5 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | We present <b>S</b>tratified <b>M</b>etric <b>T</b>emporal <b>L</b>ogic (SMTL), a novel formalism for specifying and verifying the properties of complex cyber–physical systems that exhibit behaviors across multiple temporal and abstraction scales. SMTL extends existing temporal logics by incorporating a stratification operator, enabling the association of temporal properties with specific abstraction levels. This allows for the natural expression of multi-scale requirements while maintaining formal reasoning about inter-level relationships. We formalize the syntax and semantics of SMTL, proving that it strictly subsumes metric temporal logic (MTL) and offers enhanced expressiveness by capturing properties unattainable in existing logics. Numerical simulations comparing agents operating under MTL and SMTL specifications show that SMTL enhances agent coordination and safety, reducing collision rates without substantial computational overhead or compromising path efficiency. These findings highlight SMTL’s potential as a valuable tool for designing and verifying complex multi-agent systems operating across diverse temporal and abstraction scales. |
|---|---|
| ISSN: | 2813-0405 |