SMTL: A Stratified Logic for Expressive Multi-Level Temporal Specifications
Ali Baheri, Peng Wei
TL;DR
SMTL addresses multi-scale temporal specification for cyber-physical systems by introducing a stratification operator $L_k$ that links properties to abstraction levels in a stratified timed state sequence. The authors formalize the SMTL syntax and semantics, prove that SMTL strictly subsumes metric temporal logic (MTL) and can express properties unattainable by MTL, and analyze model-checking complexity with region automata, showing EXPTIME/2EXPTIME bounds. They demonstrate practical benefits through numerical simulations of multi-agent coordination, where SMTL reduces collisions and improves path efficiency, albeit with modest computational overhead and increased waiting due to safety constraints. The work suggests substantial potential for designing and verifying multi-scale CPS and multi-agent systems, with future work on synthesis, probabilistic extensions, and scalability.
Abstract
We present Stratified Metric Temporal Logic (SMTL), a novel formalism for specifying and verifying 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 underscore SMTL's potential as a valuable tool for designing and verifying complex multi-agent systems operating across diverse temporal and abstraction scales.