STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas

Abstract

Signal Temporal Logic (STL) is a formalism used to describe temporal properties of real-valued signals in cyber-physical systems. In mission- and safety-critical domains, specifications often consist of large collections of STL formulas, making consistency checking and requirement analysis a major engineering bottleneck. Tableau-based satisfiability procedures are a natural way to address this problem. Two of the authors of this paper contributed to the only existing tree-shaped tableau for bounded discrete-time STL, but we have recently found out that the procedure can return incorrect verdicts for some STL formulas. In this paper, we pinpoint the flaw in that procedure and present a new tree-shaped tableau that we prove to be sound and complete for bounded discrete-time STL. On top of this theoretical foundation, we introduce STLSat, an open-source Rust tool that decides the satisfiability of STL formulas, synthesizes concrete witness signals, and extracts unsatisfiable cores with its tableau engine, allowing users to identify inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced first-order logic and satisfiability modulo theories encodings for STL, which allow it to act as a portfolio solver. We evaluate STLSat on an extended benchmark suite (including STL and Mission-time Linear Temporal Logic formulas) that we release publicly. Across the whole benchmark, the portfolio solver matches or outperforms state-of-the-art tools while preserving correctness.