💻 computer science

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

This paper identifies a soundness flaw in existing tableau methods for Signal Temporal Logic (STL), proposes a corrected sound and complete tree-shaped tableau, and introduces STLSat, an open-source Rust tool that leverages this theoretical foundation alongside FOL/SMT encodings to effectively check satisfiability, synthesize witnesses, and debug inconsistent specifications in cyber-physical systems.

Original authors: Marco Zamponi, Florian Lammel, Ezio Bartocci, Michele Chiari

Published 2026-07-24

📖 3 min read☕ Coffee break read

CC BY 4.0

Original authors: Marco Zamponi, Florian Lammel, Ezio Bartocci, Michele Chiari

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are the chief engineer for a fleet of self-driving cars, a smart power grid, or a robotic farm. These aren't just machines; they are "cyber-physical systems," where digital code talks to the real, messy world of physics. To keep them safe, engineers write down strict rules, like "The car must never go faster than 50 mph" or "The robot arm must stop if a human gets within two meters." But here's the catch: these rules are written in a special, super-precise language called Signal Temporal Logic (STL). It's like a mathematical recipe that describes how things should change over time.

The problem is that when you have hundreds of these rules, they might accidentally fight each other. Maybe one rule says "Speed up quickly," while another says "Never exceed 10 mph," and the system can't do both at once. If the rules are contradictory, the whole system is broken before it even starts. Checking if a giant pile of rules makes sense is like trying to solve a massive, multi-dimensional puzzle where every piece is a timeline. If the puzzle is impossible, you need to know which pieces are the culprits so you can fix them. This is the world of "satisfiability checking"—figuring out if a set of rules can actually be true at the same time.

Enter STLSat, a new digital detective built by researchers Marco Zamponi, Florian Lammel, Ezio Bartocci, and Michele Chiari. Think of STLSat as a super-smart, high-speed referee for these rule-books. The team discovered that the previous best referee (a tool called STLTree) had a secret flaw: it was taking shortcuts that sometimes let contradictory rules slip through the cracks, thinking a puzzle was solvable when it actually wasn't. STLSat fixes this by using a brand-new, mathematically proven method called a "tableau." Imagine a tableau as a giant, branching tree of "what-if" scenarios. While the old referee would sometimes skip branches to save time, the new STLSat referee uses a carefully calculated "JUMP rule" to skip time steps only when it can mathematically guarantee that no conflicts are being missed. This ensures the tool is both fast and rigorously correct, never missing a hidden conflict.

But STLSat isn't just a careful checker; it's a whole toolkit. If the rules are impossible to satisfy, STLSat doesn't just say "No." It points a finger at the specific rules causing the trouble, like a detective saying, "It's these two rules fighting each other that broke the case." It can also generate a "witness signal"—a fake, perfect example of a signal that would work if the rules were consistent, helping engineers visualize what the system should look like.

The researchers didn't just build the tool; they tested it against a massive library of over 10,000 different rule sets, including some from real-world aviation systems and thousands of randomly generated puzzles. They found that STLSat is incredibly fast, often solving problems in a fraction of a second that took older tools minutes or even timed out completely on specific large benchmarks. By running three different solving strategies at the same time (like having three detectives working on the same case simultaneously), STLSat ensures that no matter how tricky the puzzle is, it finds the answer. The result is a tool that not only guarantees the rules are correct but also helps engineers debug their designs faster, keeping our future self-driving cars and smart cities from crashing into logical dead ends.

Technical Summary: STLSat—An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas

Problem Statement

Signal Temporal Logic (STL) is the de-facto standard for specifying temporal properties of real-valued signals in cyber-physical systems (CPS). In safety-critical domains, specifications often comprise large collections of STL formulas. A major engineering bottleneck arises in verifying the consistency of these requirement sets (ensuring a signal exists that satisfies all formulas) and identifying redundancy (determining if a formula is entailed by others). Both tasks reduce to the STL satisfiability problem.

While tableau-based procedures are a natural approach for this problem, the authors identify a critical flaw in the only existing tree-shaped tableau for bounded discrete-time STL (proposed by Melani et al. [30]). The original "JUMP" optimization, designed to skip repetitive time steps, was found to be unsound: in formulas with nested temporal operators, the jump rules could skip time instants where conflicts are introduced, leading the procedure to incorrectly accept unsatisfiable formulas. Furthermore, existing tools lack mature, high-performance implementations that integrate unsatisfiable-core extraction for debugging.

Methodology

1. Corrected Tableau Algorithm

The core theoretical contribution is a sound and complete tree-shaped tableau for bounded discrete-time STL.

Basic Tableau: The authors retain the basic expansion rules (decomposing logical and temporal operators) and the STEP rule (advancing time by one unit) from the prior work, which are sound and complete.
The Flaw: The original JUMPO rule allowed skipping time steps based on interval bounds but failed to account for conflicts generated by "invariant" parts of temporal operators (e.g., the left-hand side of an Until operator) during the skipped interval.
The Correction: The authors introduce a new JUMP rule that safely compresses sequences of STEP applications. To ensure soundness and completeness, the jump size $k$ $k$ is calculated as the minimum of three distinct limits:
1. Bounds Limit ( $k$ ): Prevents jumping past the activation or expiration of operators without active parents.
2. Soundness Limit ( $k^*_{sound}$ ): Ensures that "invariant" propositions emitted by active temporal operators during the skipped interval do not conflict with propositions from other active or non-active operators. This is computed by analyzing Proposition Validity Intervals ( $T(\phi)$ ), which map the time instants where atomic propositions may appear.
3. Completeness Limit ( $k^*_{comp}$ ): Ensures that a satisfying branch is not missed by skipping a time step where a "target" proposition (e.g., the right-hand side of an Until) could be satisfied.
Correctness: The authors provide formal proofs (Theorems 2 and 3) demonstrating that the new tableau is both sound (accepts only satisfiable formulas) and complete (accepts all satisfiable formulas).

2. STLSat Tool Implementation

The authors implemented STLSat, an open-source Rust library that acts as a portfolio solver by running three complementary decision procedures in parallel:

Tableau Engine: Implements the corrected JUMP rule. It includes a lightweight syntactic simplification phase (flattening, merging intervals) and uses an explicit stack to manage memory efficiently. It also features a novel unsatisfiable-core extraction mechanism that aggregates local conflicts from rejected branches to identify the minimal subset of conflicting requirements.
First-Order Logic (FOL) Engine: An optimized encoding inspired by Li et al. [28], translating STL formulas into FOL where signals are functions from integers to real/Boolean values. It employs ad-hoc translations for F and G operators to reduce formula size.
Quantifier-Free SMT Engine: Encodes STL as a quantifier-free SMT problem over linear real arithmetic, similar to methods used for model predictive control and bounded model checking.

Key Contributions

Corrected Tableau Algorithm: A new set of rules for the JUMP optimization that formally guarantees soundness and completeness for bounded discrete-time STL, fixing the flaw in the state-of-the-art STLTree.
STLSat Tool: A high-performance, open-source Rust implementation providing a portfolio of solvers (Tableau, FOL, SMT).
Unsat-Core Extraction: A dedicated method integrated into the tableau engine to extract minimal inconsistent subsets of requirements, facilitating specification debugging.
Improved Encodings: Enhanced FOL and qualitative-semantics SMT encodings for STL.
Benchmark Suite: The release of an extensive, public benchmark suite covering both STL and Mission-time Linear Temporal Logic (MLTL) formulas, including real-world and randomly generated instances.

Experimental Results

The authors evaluated STLSat against STLTree (the original tableau implementation) and MLTLSAT (a state-of-the-art FOL-based solver for MLTL) across diverse benchmarks.

Performance: No single technique dominated all instances.
- The FOL engine excelled on the NASA-Boeing benchmark (real-world avionics requirements), solving 62/63 instances quickly, largely because these formulas rely heavily on F and G operators rather than U.
- The Tableau engine performed best on randomly generated formulas with wide time intervals, leveraging the JUMP rule to skip redundant steps efficiently.
- The SMT engine generally underperformed compared to the other two.
Portfolio Approach: Running all three engines in parallel yielded the best overall performance, matching or outperforming state-of-the-art tools while preserving the correctness guarantees of the sound tableau.
Debugging: In a running example involving an irrigation controller, STLSat identified the set of requirements as unsatisfiable in a fraction of a second and correctly extracted the unsatisfiable core $\{\phi_1, \phi_2\}$ , pinpointing the conflict between flow rate requirements and safety bounds.

Significance

The paper claims that STLSat addresses a critical gap in the verification of cyber-physical systems by providing a sound satisfiability checker where previous state-of-the-art tools contained unsound optimizations. By combining a corrected theoretical foundation with a practical, high-performance tool that supports unsatisfiable-core extraction, STLSat enables effective specification mining, redundancy elimination, and automated debugging. The authors emphasize that their work transforms raw, potentially inconsistent sets of mined constraints into concise, traceable requirement models, a capability previously lacking in mature, dedicated solvers.