A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators

TL;DR

This paper presents a novel tree-shaped tableau method for efficiently checking the satisfiability of discrete-time Signal Temporal Logic (STL) with bounded operators, improving performance over existing SMT and First-Order Logic approaches.

Contribution

The authors introduce a new one-pass tableau approach for STL satisfiability that exploits redundancy in large time intervals, applicable to consistency, synthesis, and implication verification.

Findings

Tableau outperforms SMT and FOL encodings on benchmarks.

Method speeds up satisfiability checking by exploiting temporal redundancy.

Applicable to STL and Mission-Time Linear Temporal Logic.

Abstract

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.