A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912508299706368 |
|---|---|
| author | Melani, Beatrice Bartocci, Ezio Chiari, Michele |
| author_facet | Melani, Beatrice Bartocci, Ezio Chiari, Michele |
| contents | Signal Temporal Logic (STL) is a widely recognized formal specification language to express rigorous temporal requirements on mixed analog signals produced by cyber-physical systems (CPS). A relevant problem in CPS design is how to efficiently and automatically check whether a set of STL requirements is logically consistent. This problem reduces to solving the STL satisfiability problem, which is decidable when we assume that our system operates in discrete time steps dictated by an embedded system's clock.
This paper introduces a novel tree-shaped, one-pass tableau method for satisfiability checking of discrete-time STL with bounded temporal operators. Originally designed to prove the consistency of a given set of STL requirements, this method has a wide range of applications beyond consistency checking. These include synthesizing example signals that satisfy the given requirements, as well as verifying or refuting the equivalence and implications of STL formulas.
Our tableau exploits redundancy arising from large time intervals in STL formulas to speed up satisfiability checking, and can also be employed to check Mission-Time Linear Temporal Logic (MLTL) satisfiability. We compare our tableau with Satisfiability Modulo Theories (SMT) and First-Order Logic encodings from the literature on a benchmark suite, partly collected from the literature, and partly provided by an industrial partner. Our experiments show that, in many cases, our tableau outperforms state-of-the-art encodings. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_21598 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators Melani, Beatrice Bartocci, Ezio Chiari, Michele Logic in Computer Science Signal Temporal Logic (STL) is a widely recognized formal specification language to express rigorous temporal requirements on mixed analog signals produced by cyber-physical systems (CPS). A relevant problem in CPS design is how to efficiently and automatically check whether a set of STL requirements is logically consistent. This problem reduces to solving the STL satisfiability problem, which is decidable when we assume that our system operates in discrete time steps dictated by an embedded system's clock. This paper introduces a novel tree-shaped, one-pass tableau method for satisfiability checking of discrete-time STL with bounded temporal operators. Originally designed to prove the consistency of a given set of STL requirements, this method has a wide range of applications beyond consistency checking. These include synthesizing example signals that satisfy the given requirements, as well as verifying or refuting the equivalence and implications of STL formulas. Our tableau exploits redundancy arising from large time intervals in STL formulas to speed up satisfiability checking, and can also be employed to check Mission-Time Linear Temporal Logic (MLTL) satisfiability. We compare our tableau with Satisfiability Modulo Theories (SMT) and First-Order Logic encodings from the literature on a benchmark suite, partly collected from the literature, and partly provided by an industrial partner. Our experiments show that, in many cases, our tableau outperforms state-of-the-art encodings. |
| title | A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.21598 |