1 Introduction↩︎

Signal Temporal Logic (STL) [1] is a well-established specification language to describe the temporal properties of real‑valued signals in mission‑ and safety‐critical cyber‑physical systems (CPS). STL underpins a broad spectrum of verification tasks, ranging from runtime monitoring [2] and mutation testing [3] to falsification [4], parameter synthesis [5], fault localisation [6] and debugging [7]. During the design of a CPS, engineers typically collect a large number of STL requirements. In this context, the two following situations can be problematic:

Inconsistency. A set of STL formulas \(\Phi=\{\varphi_1,\dots,\varphi_n\}\) is consistent iff there exists at least one signal \(s\) such that \(s\models\bigwedge_{i=1}^{n}\varphi_i\). Equivalently, the conjunction \(\bigwedge_{i=1}^{n}\varphi_i\) must be satisfiable; if it is not, the requirements are mutually contradictory.

Redundancy. A formula \(\psi\in\Phi\) is redundant w.r.t.the remaining requirements iff those requirements already entail \(\psi\), i.e., \(\bigwedge_{\varphi\in\Phi\setminus\{\psi\}} \models \psi\). By definition, this holds exactly when the formula \(\bigl(\bigwedge_{\varphi\in\Phi\setminus\{\psi\}}\bigr)\land\neg\psi\) is unsatisfiable.

Both notions can be reduced to a single STL‑satisfiability query: for any pair of formulas \(\varphi,\psi\), the implication \(\varphi\models\psi\) holds iff \(\varphi\land\neg\psi\) is unsatisfiable, and equivalence follows from mutual implication.

These reductions are especially valuable for specification mining [8], when automatically extracting temporal-logic specifications from execution traces or natural-language descriptions. Automatically extracted requirements often contain noise, redundancies, or inconsistencies that compromise their usefulness. In this context, the satisfiability check of STL formulas enables pruning inconsistent subsets, eliminating redundancies, and clustering semantically equivalent specifications, thereby turning a raw set of mined constraints into a concise, traceable requirement model.

Example. Consider an autonomous crop‑irrigation controller whose water‑flow signal \(f\) is measured along the irrigation line. The following three STL requirements have been elicited: \[\tag{1} \begin{align} \varphi_1 &:= \mathop{\mathsf{\mathsf{G}}^{{}}_{[0,100]}}\,\mathop{\mathsf{\mathsf{F}}^{{}}_{[10,40]}} (f \ge 50) \tag{2}\\ \varphi_2 &:= \mathop{\mathsf{\mathsf{G}}^{{}}_{[0,120]}}\bigl( f \ge 50 \;\Rightarrow\; \mathop{\mathsf{\mathsf{F}}^{{}}_{[0,10]}}\,\mathop{\mathsf{\mathsf{G}}^{{}}_{[0,30]}} (f < 5) \bigr) \tag{3}\\ \varphi_3 &:= \mathop{\mathsf{\mathsf{G}}^{{}}_{[0,120]}} (f < 100) \tag{4} \end{align}\]

• 2 requires that the water flow always within \([0,100]\) time units should periodically reach or exceed 50 l/min in a window of \(10\)–\(40\) time units.

• 3 states that whenever the flow reaches this irrigation value, it must be reduced below \(5\) l/min within the next \(10\) time units and stay low for another \(30\) time units, in order to avoid over‑watering.

• 4 is a safety bound that forbids flows equal to or above \(100\) l/min at any time in the interval 0-120 units, preventing flooding of the field.

The three formulas together form the specification \(\Phi=\{\varphi_1,\varphi_2,\varphi_3\}\). Before \(\Phi\) can be used for model checking or falsification, we must verify that it is consistent, i.e.that the conjunction \(\bigwedge_{i=1}^{3}\varphi_i\) is satisfiable. Intuitively, 3 forces a very rapid drop from \(f\ge 50\) to \(f<5\), which may be physically impossible given actuator limits; however, turning this intuition into a rigorous proof requires exploring all possible signal behaviors over the continuous domain \([0,120]\). Manual reasoning is error‑prone, whereas automated STL satisfiability tools decide consistency in seconds; if the set is satisfiable they synthesize a concrete witness signal, and if it is unsatisfiable they extract an unsatisfiable core that pinpoints the conflicting requirements, enabling their immediate refinement.

Although STL has become the de‑facto standard specification language for CPS requirements, it is still lacking mature, high‑performance and dedicated satisfiability solvers. Existing approaches either target different logics—e.g., MLTLSAT [9]—or exist only as research prototypes such as the tableau implementation described in [10]. Moreover, these tools do not integrate smoothly into verification pipelines, which limits their usefulness for practical requirement‑engineering workflows that require automated debugging and traceability.

The most prominent tableau‑based solver for bounded discrete‑time STL is STLTree [10]. Its one‑pass construction accelerates reasoning by “jumping” over intervals, but a careful analysis reveals a soundness flaw: in formulas with nested temporal operators, the old jump rules may skip instants where conflicts would be introduced, causing the tableau to miss rejecting branches. This motivates our first contribution: a corrected tableau algorithm with formally proved soundness and completeness. Our approach inspects proposition-appearance intervals to formally guarantee that no conflicts can be introduced in skipped time steps.

Building on this foundation we introduce STLSat, an open‑source Rust library that implements three complementary decision procedures: our correct tableau, an optimised first‑order‑logic encoding, and a qualitative‑semantics SMT encoding. The engines can be executed in parallel, providing both speed and flexibility; the tableau additionally supports unsatisfiable‑core extraction for debugging. To foster reproducible research we also release an extensive benchmark suite covering STL. To the best of our knowledge no such public collection exists in the literature.

As a showcase, STLSat proves in a fraction of one second that the 2 –4 irrigation requirements are mutually inconsistent. In addition to reporting unsatisfiability, the tableau engine also returns as unsat core the subset of constraints \(\{ \varphi_1, \varphi_2 \}\) responsible for the conflict, thus providing immediate debugging support.

We conduct an extensive empirical evaluation on the released benchmark set of STL formulas, as well as its close relative MLTL coming from related works, comparing each STLSat engine against state‑of‑the‑art STL solvers and against a dedicated MLTL satisfiability checker [11]. The results show that no single technique dominates across all instances; however, the portfolio approach combining the three STLSat solving engines achieves the best overall performance in terms of runtime and scalability.

In summary, our contributions are:

1. a correct tree-shaped tableau algorithm with a novel set of rules;

2. a high‑performance Rust implementation for bounded discrete‑time STL satisfiability;

3. a novel unsat‑core extraction method for the tableau engine;

4. an improved FOL encoding and a qualitative‑semantics SMT encoding;

5. a parallel execution framework that can run all engines concurrently;

6. an open benchmark suite covering STL formulas; and

7. a thorough experimental study demonstrating superior performance over existing tools.

The remainder of the paper is organised as follows. Section 2 surveys related work on temporal logic satisfiability. Section 3 recalls the syntax and semantics of STL and MLTL. Section 4 details the flaws in the existing tableau [10] and presents our corrected tableau algorithm together with its soundness and completeness proofs. Section 5 details the implementation of STLSat’s three solving engines. Section 6 describes our experimental methodology and reports the results. Finally, Section 7 draws conclusions and outlines future research directions.

2 Related Work↩︎

Originally proposed for CPS monitoring and testing [1], STL has primarily been studied in the context of runtime verification [12], leaving systematic consistency checking, redundancy removal, and implication analysis in requirements engineering largely unaddressed.

Validity, vacuity, and redundancy. A first step toward addressing these issues was taken by [13], who reduced validity, vacuity, and redundancy questions for STL to satisfiability problems in Metric Interval Temporal Logic (MITL) [14]. Their approach leverages existing MITL solvers [15] to obtain counterexamples or proofs of equivalence. While effective, this pipeline incurs the overhead of translating STL into a different logic and does not directly support the extraction of minimal conflicting subsets.

Debugging tools. In the same spirit, [16] proposed STLInspector, a debugging aid that generates concrete witness signals by mutating candidate models and querying an SMT encoding of the STL formula. The tool is useful for pinpointing why a specification holds or fails on a given trace, but it does not provide a systematic analysis of the logical relationships among multiple requirements.

Satisfiability/Model checking. The close relationship between satisfiability and bounded model checking has motivated several encodings of STL into first‑order logic (FOL) or Satisfiability Modulo Theories (SMT). [17] presented a refutationally complete SMT encoding for bounded model checking of continuous‑time STL against hybrid system models; an improved variant was later shown to be suitable for satisfiability checking [18]. For discrete‑time settings, [19] introduced an SMT formulation aimed at model predictive control that can also serve as a decision procedure for STL satisfiability [10].

Tableau‑based approaches. The only dedicated tableau method for bounded discrete‑time STL prior to our work is the one‑pass tree‑shaped construction proposed by [10]. Their algorithm, inspired by tableau techniques for other temporal logics [20], [21], established that STL satisfiability is EXPSPACE‑complete and was implemented in a prototype Python tool. In the course of our investigation we discovered a soundness flaw in their original jump optimisation; we therefore revisited the mathematical definition, and proved both soundness and completeness for the corrected rule.

Related temporal logics. Several works have studied satisfiability for logics closely related to STL. [22], [23] offered SMT encodings for MITL and Quantified Temporal Logic (QTL) [24], but these frameworks admit only Boolean signals, limiting their applicability to the quantitative nature of STL. Mission‑time Linear Temporal Logic (MLTL) [11] shares many syntactic constructs with STL; a systematic comparison of encodings for MLTL—including translations to LTL on finite traces, SMV specifications, and FOL—was carried out by [25], who identified the FOL encoding as the most performant. Our tool incorporates an improved version of this FOL translation and demonstrates superior empirical performance on both STL and MLTL benchmarks.

Unsatisfiable‑core extraction. The extraction of minimal unsatisfiable cores has been extensively investigated for propositional SAT and SMT solving [26]. Within temporal logics, similar techniques have been explored mainly for Linear Temporal Logic (LTL) [27], [28], but to the best of our knowledge no existing framework provides unsat‑core extraction for STL formulas. By integrating a dedicated core extraction mechanism into our tableau engine we fill this gap and enable direct debugging of inconsistent requirement sets.

3 Background↩︎

3.0.0.1 Signal Temporal Logic (STL).

We define bounded discrete-time STL [1] on the temporal domain of natural numbers \(\mathbb{N}\). A signal is a function \(w : \mathbb{N} \rightarrow \mathbb{R}^n\) that associates time instants with valuations of a finite set of signal variables \(S = \{ x_1, \dots, x_n \}\). We define the projection \(w_R\) of a signal \(w\) on a set \(R \subseteq S\) in the usual way. STL formulas have the following syntax: \[\varphi := \top \mid f(R) \bowtie k \mid \neg \varphi \mid \varphi_1 \lor \varphi_2 \mid {\varphi_1} \mathbin{{\mathsf{U}}^{}_{I}} {\varphi_2}\] where \(\mathord{\bowtie} \in \{\mathord{<}, \mathord{=}, \mathord{>}\}\), \(R \subseteq S\) is a set of signal variables, \(f : \mathbb{R}^{|R|} \rightarrow \mathbb{R}\) a linear function of signal values, \(k \in \mathbb{Q}\) a rational constant, and \(I = [a,b]\) with \(a, b \in \mathbb{N}\).

We define the semantics on a signal \(w\) and a time instant \(t \in \mathbb{N}\) as follows: \[\begin{align} &(w,t) \models \top && \text{(always true)} \\ &(w,t) \models f(R) \bowtie k & \text{iff } & f(w_R(t)) \bowtie k, \text{ with } \mathord{\bowtie} \in \{\mathord{<}, \mathord{=}, \mathord{>}\} \\ &(w,t) \models \neg \varphi & \text{iff } & (w,t) \not\models \varphi \\ &(w,t) \models \varphi_1 \lor \varphi_2 & \text{iff } & (w,t) \models \varphi_1 \text{ or } (w,t) \models \varphi_2 \\ &(w,t) \models {\varphi_1} \mathbin{{\mathsf{U}}^{}_{[a,b]}} {\varphi_2} & \text{iff } & \exists t' \in [t+a, t+b] : (w, t') \models \varphi_2 \text{ and } \forall t'' \in [t, t'] : (w,t'') \models \varphi_1 \end{align}\] Boolean signals can be encoded by defining a real variable \(x_p\) for each atomic proposition \(p\), and asserting \(p\) as \(x_p = 1\) and \(\neg p\) as \(x_p \neq 1\).

We use additional propositional operators (\(\land\), \(\rightarrow\)) and temporal operators eventually (or finally) \(\mathop{\mathsf{\mathsf{F}}^{{}}_{I}}\) and always (or globally) \(\mathop{\mathsf{\mathsf{G}}^{{}}_{I}}\) as shortcuts for \(\mathop{\mathsf{\mathsf{F}}^{{}}_{I}} \varphi \equiv {\top} \mathbin{{\mathsf{U}}^{}_{I}} {\varphi}\) and \(\mathop{\mathsf{\mathsf{G}}^{{}}_{I}} \varphi \equiv \neg \mathop{\mathsf{\mathsf{F}}^{{}}_{I}} \neg \varphi\). We also employ the release operator \(\mathsf{R}\), defined as the dual of until under negation, i.e., \({\varphi_1} \mathbin{{\mathsf{R}}^{}_{I}} {\varphi_2} \equiv \neg ({\neg \varphi_1} \mathbin{{\mathsf{U}}^{}_{I}} {\neg \varphi_2})\).

Given \({\varphi_1} \mathbin{{\mathsf{U}}^{}_{I}} {\varphi_2}\) and \({\varphi_2} \mathbin{{\mathsf{R}}^{}_{I}} {\varphi_1}\), we refer to \(\varphi_1\) as the invariant, and to \(\varphi_2\) as the target.

3.0.0.2 Mission-Time Linear Temporal Logic (MLTL).

MLTL [11] can be seen as a fragment of bounded discrete-time STL that only allows for Boolean signals. It also differs from STL in the semantics of the until operator, which we denote as strict until (\(\mathsf{sU}{}\)) for MLTL: \[(w,t) \models {\varphi_1} \mathbin{{\mathsf{sU}}^{}_{[a,b]}} {\varphi_2} \text{ iff } \exists t' \in [t+a, t+b] : (w, t') \models \varphi_2 \text{ and } \forall t'' \in [t+a, t'-1] : (w,t'') \models \varphi_1\] The strict release operator is defined as \({\varphi_1} \mathbin{{\mathsf{sR}}^{}_{I}} {\varphi_2} \equiv \neg ({\neg\varphi_1} \mathbin{{\mathsf{sU}}^{}_{I}} {\neg\varphi_2})\).

Indeed, MLTL’s until operator is expressible in terms of STL’s, and vice versa: \[\begin{align} {\varphi_1} \mathbin{{\mathsf{sU}}^{}_{[a,b]}} {\varphi_2} &\equiv \mathop{\mathsf{\mathsf{F}}^{{}}_{[a,a]}} \big({(\varphi_1 \lor \varphi_2)} \mathbin{{\mathsf{U}}^{}_{[0, b-a]}} {\varphi_2}\big) & {\varphi_1} \mathbin{{\mathsf{sR}}^{}_{[a,b]}} {\varphi_2} &\equiv \mathop{\mathsf{\mathsf{F}}^{{}}_{[a,a]}} \big({(\varphi_1 \land \varphi_2)} \mathbin{{\mathsf{R}}^{}_{[0, b-a]}} {\varphi_2}\big) \\ {\varphi_1} \mathbin{{\mathsf{U}}^{}_{[a,b]}} {\varphi_2} &\equiv \mathop{\mathsf{\mathsf{G}}^{{}}_{[0,a]}} \varphi_1 \land {\varphi_1} \mathbin{{\mathsf{sU}}^{}_{[a,b]}} {(\varphi_1 \land \varphi_2)} & {\varphi_1} \mathbin{{\mathsf{R}}^{}_{[a,b]}} {\varphi_2} &\equiv \mathop{\mathsf{\mathsf{F}}^{{}}_{[0,a]}} \varphi_1 \lor {\varphi_2} \mathbin{{\mathsf{sU}}^{}_{[a,b]}} {\varphi_1} \lor \mathop{\mathsf{\mathsf{G}}^{{}}_{[a,b]}} \varphi_2 \end{align}\] The equivalences in the second row, together with common propositional and temporal logic equivalences, allow for rewriting all STL formulas in strict normal form, i.e., by using only strict operators in positive form, with negation only applied to atomic propositions.

4 Tree-Shaped Tableau↩︎

Building upon the tree-shaped tableau introduced in [10], we propose an alternative definition of the JUMP rule that fixes the soundness and completeness problems in the original one.

We begin by reviewing the original basic tableau, i.e., without the JUMP rule, whose soundness and completeness results still hold. We then introduce the new JUMP rule and, finally, present its correctness theorems.

4.1 Basic Tableau↩︎

A tableau is a tree in which each node \(u\) is labeled with a set of formula occurrences \(\Gamma(u)\) required to hold conjunctively, and a time counter \(t(u) \in \mathbb{N}\). The root \(u_0\) is labeled with the formula \(\phi\) to be checked, assumed to be in strict normal form. Besides a formula, elements of \(\Gamma(u)\) may carry auxiliary metadata recording the temporal formula occurrence that generated them—i.e., their parent. We write \(\langle \varphi\rangle_{\psi}\) for the occurrence whose underlying formula is \(\varphi\) and whose parent occurrence is \(\psi\), and \(\langle \varphi\rangle_{\bot}\) when no parent is present (e.g., for operators in the input formula). Parent annotations are only needed by the JUMP rule, hence we omit them whenever not strictly relevant, and we identify occurrences in \(\Gamma(u)\) by their underlying formula.

The tableau is built incrementally by applying to each node expansion rules that generate child nodes by decomposing formulas in the parent’s node label. These expansion rules are summarized in Table 1. They expand formulas to simpler ones according to their semantics.

The decomposition of temporal operators employs a temporal expansion function \(\operatorname{tex}\), which updates intervals when nested temporal operators are unfolded: \[\begin{align} \begin{alignedat}{3} &\operatorname{tex}^t(\top) = \top &\qquad &\operatorname{tex}^t(f(R) \bowtie k) = f(R) \bowtie k &\qquad &\operatorname{tex}^t(\neg \varphi_1) = \neg \operatorname{tex}^t(\varphi_1) \end{alignedat} \\&\operatorname{tex}^t(\varphi_1 \circ \varphi_2) = \operatorname{tex}^t(\varphi_1) \circ \operatorname{tex}^t(\varphi_2) &\qquad& \text{with } \circ \in \{ \land, \lor \} \\ &\operatorname{tex}^t(\mathop{\mathsf{A}^{}_{[a,b]}}{\varphi}) = \mathop{\mathsf{A}^{}_{[a+t,b+t]}}{\varphi} &\qquad& \text{with } \mathsf{A} \in \{ \mathsf{F}, \mathsf{G} \} \\ &\operatorname{tex}^t({\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{[a,b]}} {\varphi_2}) = {\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{[a+t,b+t]}} {\varphi_2} &\qquad& \text{with } \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \}.\end{align}\]

During tableau construction, nodes are checked for local inconsistencies. Formally, a node \(u\) is rejected (and closed) if either \(\neg \top \in \Gamma(u)\) or the set of propositions \(\{ f(R) \bowtie k \in \Gamma(u) \} \cup \{ \lnot(f(R) \bowtie k) \in \Gamma(u) \}\) is inconsistent. Rejected nodes are leaves.

When no further decomposition rule is applicable to a node, i.e., all temporal operators in its label are marked or not active, the node is said to be poised. In this case, the tableau advances time through the STEP rule:

STEP

Let \(u\) be a poised node. If \(\Gamma(u)\) contains any temporal operators, then \(u\) has one child \(u'\) with \(t(u')=t(u)+1\), and \[\begin{align} \Gamma(u') = \;& \{ \mathop{\mathsf{A}^{}_{I}}{\varphi} \in \Gamma(u) \mid \mathsf{A} \in \{ \mathsf{F}, \mathsf{G} \} \} \cup \{ {\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{I}} {\varphi_2} \in \Gamma(u) \mid \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \} \} \\ &\cup \{ \mathop{\mathsf{A}^{}_{[a,b]}}{\varphi} \mid \mathop{\mathsf{\overline{\mathsf{A}}}^{}_{[a,b]}}{\varphi} \in \Gamma(u) \land \mathsf{A} \in \{ \mathsf{F}, \mathsf{G} \} \land t(u) < b \} \\ &\cup \{ {\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{[a,b]}} {\varphi_2} \mid {\varphi_1} \mathbin{{\overline{\mathsf{B}}}^{}_{[a,b]}} {\varphi_2} \in \Gamma(u) \land \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \} \land t(u) < b \} \end{align}\]

If \(u\) is poised, not rejected, and its STEP successor label is empty, then the corresponding branch is accepted and witnesses the satisfiability of the input formula. If the tableau frontier consists of only rejected nodes, the input formula is unsatisfiable.

Fig. 1 shows an example of the basic tableau for formula \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[0,4]}}a \land {b} \mathbin{{\mathsf{sU}}^{}_{[4,7]}} {\neg a}\).

Soundness and completeness of the basic tableau were established in [10]:

4.2 The \(\mathsf{JUMP}_\mathsf{O}\) Rule and its Unsoundness↩︎

As an optimization to the basic tableau, [10] introduced the \(\mathsf{JUMP}_\mathsf{O}\) rule, whose purpose is to skip repetitive parts of the tableau by jumping directly to a later point in time. For instance, when building the tableau for formula \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[0,20]}}{x > 0} \land \mathop{\mathsf{\mathsf{F}}^{{}}_{[0,5]}}{x > 5}\), one need not develop the tableau for all instants from 0 to 5 and from 5 to 20 to realize that a satisfying signal exists. With the \(\mathsf{JUMP}_\mathsf{O}\) rule, the tableau skips intermediate time steps, only checking consistency at interval bounds, namely 0, 5, and 20. Formulas with nested operators are trickier: the tableau by [10] waits until the end of the time interval of the first extracted instance of the inner operator. For instance, with formula \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[5,20]}}{\mathop{\mathsf{\mathsf{F}}^{{}}_{[0,5]}} x > 0}\), the tableau proceeds with the STEP rule until time \(5 + 5 = 10\), after which it may jump to time 20.

We found out, however, that this precaution is not enough to preserve the soundness of the tableau. Consider the following unsatisfiable formula: \[\varphi_S = {(\mathop{\mathsf{\mathsf{G}}^{{}}_{[0,0]}} \mathop{\mathsf{\mathsf{G}}^{{}}_{[5,5]}} a)} \mathbin{{\mathsf{sU}}^{}_{[0,4]}} {(\mathop{\mathsf{\mathsf{G}}^{{}}_{[5,5]}} \neg c)} \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[5,8]}} c \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} \neg a\] With the \(\mathsf{JUMP}_\mathsf{O}\) rule, a tableau branch skips times from 1 to 3. At time 3, the basic tableau extracts \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} a\) from the \(\mathsf{sU}\) operator, which conflicts with \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} \neg a\). However, the \(\mathsf{JUMP}_\mathsf{O}\) rule skips this step, and creates a node with time 4 that does not contain \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} a\) and does not incur any conflict, leading to an accepted branch that does not correspond to a model of \(\varphi_S\).

The \(\mathsf{JUMP}_\mathsf{O}\) rule compromises both soundness and completeness of the tableau. We describe this flaw in more detail in Appendix 8.

4.3 A new, correct JUMP Rule↩︎

To speed up tableau construction, we introduce the JUMP rule, which can be used to compress a sequence of STEP rule applications. Intuitively, a jump from a poised node \(u\) to a node \(u'\) has the same effect as postponing all active temporal operators until time \(t(u')\) by always choosing the expansion rule \(\Gamma_{\phi}(u_p)\).

To describe the JUMP rule, we introduce new notation, then discuss the jump-size computation, and finally describe the resulting node. To simplify notation, we omit the \(\mathsf{G}\) and \(\mathsf{F}\) operators, which we replace by the standard equivalences \(\mathop{\mathsf{\mathsf{G}}^{{}}_{I}}\varphi \equiv {\neg\top} \mathbin{{\mathsf{sR}}^{}_{I}} {\varphi}\) and \(\mathop{\mathsf{\mathsf{F}}^{{}}_{I}}\varphi \equiv {\top} \mathbin{{\mathsf{sU}}^{}_{I}} {\varphi}\).

The JUMP rule needs parent annotations, which are created by expansion rules. They are accessed through the parent-active predicate \(P\), which we define over a formula occurrence and a node as follows: \[\begin{align} P(\phi,u) \quad\text{iff}\quad \phi = \langle \varphi\rangle_{\psi} \text{ for some } \phi \in \Gamma(u) \text{ s.t. } \psi \neq \bot \text{ and } \psi \in \Gamma(u). \end{align}\]

4.3.0.1 Proposition Validity Intervals.

We define the proposition validity interval \(\mathcal{T}(\varphi)\) of a formula \(\varphi\), representing the time intervals in which propositions in \(\varphi\) may appear. Formally: \[\begin{align}&\mathcal{T}(f(R) \bowtie k) = \{ (0,0) \} &\qquad &\mathcal{T}(\neg \varphi) = \mathcal{T}(\varphi) \\ &\mathcal{T}(\varphi_1 \circ \varphi_2) = \mathcal{T}(\varphi_1) \cup \mathcal{T}(\varphi_2) &\qquad& \text{with } \circ \in \{ \land, \lor \} \\\\ \begin{align} \mathcal{T}({\varphi_1} \mathbin{{\mathsf{sU}}^{}_{[a,b]}} {\varphi_2}) = \mathcal{T}({\varphi_1} \mathbin{{\mathsf{sR}}^{}_{[a,b]}} {\varphi_2}) &= \{ (l+a, r+b-1) \mid (l,r) \in \mathcal{T}(\varphi_1),\;a < b \} \\ &\quad\cup \{ (l+a, r+b) \mid (l,r) \in \mathcal{T}(\varphi_2) \} \end{align} \end{align}\]

The purpose of \(\mathcal{T}\) is to identify the time instants at which atomic propositions may appear and conflict with other propositions.

To distinguish different occurrences of the same proposition, we associate a unique identifier to every occurrence. For instance, in \(\varphi = {p} \mathbin{{\mathsf{sU}}^{}_{[0,5]}} {q} \land {p} \mathbin{{\mathsf{sU}}^{}_{[0,10]}} {r}\), the two occurrences of \(p\) are treated as distinct because they are governed by different temporal constraints. Formally, the formula is viewed as a syntax tree whose leaves carry unique identifiers. Two propositions are considered equivalent only if they share the same syntactic structure and identifier. Identifiers are preserved by expansion rules and by the temporal expansion operator \(\operatorname{tex}\). Such identifiers are used only for validity intervals: for local consistency checking, propositions are compared solely based on their syntactic structure.

Function \(\mathcal{T}\) is defined so that each occurrence of an atomic proposition \(\rho\) in a formula contributes exactly one pair \((l,r)\). Hence, we may unambiguously refer to a pair \(i = (l,r) \in \mathcal{T}(\varphi)\) deriving from \(\rho\), meaning the specific occurrence identified via its identifier rather than merely its syntactic structure.

The following lemma, whose proof is in Appendix 9, relates validity intervals computed from a formula \(\varphi\) to the time instants at which occurrences of a proposition produced by decompositions of \(\varphi\) may appear in the tableau:

4.3.1 Jump Size Calculation↩︎

To guarantee that the JUMP rule preserves the correctness of the algorithm, we compute the jump size \(k\) as the minimum of three distinct values.

4.3.1.1 Bounds Limit (\(k\))

The first limit ensures that the jump does not cross a time instant at which an operator without an active parent becomes active or expires. It is defined as \[k(u) = \min\{t\in K(u)\mid t>t(u)\} - t(u),\] where the set \(K(u)\) collects bounds of temporal operators whose parents are not active in \(u\): \[\begin{align} K(u)=&\;\{ a,b\mid \varphi = {\varphi_1} \mathbin{{\mathsf{B}}^{{\psi}}_{[a,b]}} {\varphi_2}\in\Gamma(u),\;\mathsf{B}\in\{ \mathsf{sR},\overline{\mathsf{sR}} \},\;\lnot P(\varphi, u) \} \\ &\cup\{ a, b\mid {\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{[a,b]}} {\varphi_2}\in\Gamma(u),\;\mathsf{B}\in\{ \mathsf{sU},\overline{\mathsf{sU}} \} \} \end{align}\]

4.3.1.2 Soundness Limit (\(k^{\ast}_{\text{sound}}\))

Consider a temporal operator \(\varphi = {\varphi_1} \mathbin{{\overline{\mathsf{sU}}}^{}_{[a,b]}} {\varphi_2}\) or \(\varphi = {\varphi_2} \mathbin{{\overline{\mathsf{sR}}}^{}_{[a,b]}} {\varphi_1}\) in a poised node \(u\). The basic tableau would emit the invariant part \(\varphi_1\) at every intermediate time instant \(t(u)+j\), with \(1 \leq j < k\), before reaching the jump destination \(t(u)+k\). To guarantee the soundness of the approach, we need to be sure that such invariants do not generate conflicts with other formulas in the node.

We first collect the validity intervals of atomic propositions that may be generated by the invariant part of active postponed temporal operators: \[\begin{align} N(u) = \bigcup\limits_{\varphi \in \Gamma(u)} \{ (t(u) + l, t(u) + r) \mid (l, r) \in \mathcal{T}(\varphi_1), \varphi = {\varphi_1} \mathbin{{\overline{\mathsf{sU}}}^{}_{[a,b]}} {\varphi_2} \lor \varphi = {\varphi_2} \mathbin{{\overline{\mathsf{sR}}}^{}_{[a,b]}} {\varphi_1} \}. \end{align}\] An element \((l_n,r_n)\in N(u)\) describes the validity interval of an invariant emitted at time instant \(t(u)\) by an active temporal operator \(\varphi\), i.e., \(\operatorname{tex}^{t(u)}(\varphi_1)\). If the same invariant is emitted at a skipped time \(t(u)+j\), its interval is shifted to \((l_n+j,r_n+j)\).

We then collect the validity intervals of atomic propositions that may be generated by temporal operators in \(\Gamma(u)\) whose parent is not active: \[\begin{align} O(u) = \bigcup\limits_{\varphi \in \Gamma(u)} \{ (l,r) \mid (l,r) \in \mathcal{T}(\varphi), \varphi = {\varphi_2} \mathbin{{\mathsf{B}}^{{}}_{[a,b]}} {\varphi_1}, \mathsf{B} \in \{ \mathsf{sU}, \overline{\mathsf{sU}}, \mathsf{sR}, \overline{\mathsf{sR}} \}, \lnot P(\varphi, u) \} \end{align}\]

If an interval in \(N(u)\) intersects one in \(O(u)\), we cannot exclude that the skipped invariant conflicts with other formulas. Since we do not know which propositions will eventually form an inconsistent core, we perform a STEP as a safe choice: the JUMP rule is disabled whenever \[\label{eq:sound-condition} \exists (n, o) \in N(u) \times O(u) \text{ s.t. } n \cap o \neq \emptyset\tag{5}\]

If no such intersection exists, for every \(n=(l_n,r_n)\in N(u)\) and \(o=(l_o,r_o)\in O(u)\), either \(r_n<l_o\) or \(r_o<l_n\). The case \(r_o < l_n\) is always safe: delaying the emitted invariants moves the interval to the future, so other proposition intervals will never intersect with it. In case \(r_n < l_o\) instead, shifting the invariant to the future might cause the intersection of the intervals. We define the sound jump limit as the earliest distance at which propositions may appear together: \[\begin{align} k^{\ast}_{\text{sound}}(u) = \min\big(\{ l_o - r_n \mid (n, o) \in N(u) \times O(u) \land r_n < l_o \} \cup \{ +\infty \}\big) \end{align}\]

4.3.1.3 Completeness Limit (\(k^{\ast}_{\text{comp}}\))

Consider a temporal operator \(\varphi = {\varphi_1} \mathbin{{\overline{\mathsf{sU}}}^{}_{[a,b]}} {\varphi_2}\) or \(\varphi = {\varphi_2} \mathbin{{\overline{\mathsf{sR}}}^{}_{[a,b]}} {\varphi_1}\) in a poised node \(u\). The JUMP rule reconstructs the branch in which this temporal obligation is postponed until the jump destination \(t(u) + k\). In the basic tableau, an accepting branch may satisfy the temporal obligation (i.e., select the \(\Gamma_{\varphi}(u_s)\) expansion rule) at some intermediate time \(t(u)+j\), with \(1 \leq j < k\). If time step time \(t(u)+j\) is skipped, the JUMP rule may reach a node rejected due to the postponed obligation, even though the basic tableau had an accepting branch rooted at \(t(u)+j\).

We first collect the validity intervals of atomic propositions that may be generated by the target (i.e., \(\varphi_2\)) part of active temporal operators: \[\begin{align} M(u) = \bigcup\limits_{\varphi \in \Gamma(u)} \{ (t(u) + l, t(u) + r) \mid (l, r) \in \mathcal{T}(\varphi_2), \varphi = {\varphi_1} \mathbin{{\overline{\mathsf{sU}}}^{}_{[a,b]}} {\varphi_2} \lor \varphi = {\varphi_2} \mathbin{{\overline{\mathsf{sR}}}^{\psi}_{[a,b]}} {\varphi_1} \}. \end{align}\] An element \((l_m,r_m)\in M(u)\) describes the validity interval of a proposition generated by the formula emitted at time \(t(u)\), namely \(\operatorname{tex}^{t(u)}(\varphi_2)\). If the same target is emitted at some time \(t(u)+j\) with \(1 \leq j < k\), its interval is shifted to \((l_m+j,r_m+j)\).

We then collect the validity intervals of propositions that may generate conflicts with a target extraction. These consist of propositions already present in the node and the ones generated by non-expired temporal operators without an active parent: \[\begin{align} S(u) ={}& \bigcup\limits_{\varphi \in \Gamma(u)} \{ (l+a, r+b) \mid (l,r) \in \mathcal{T}(\varphi_1),\; \varphi = {\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{[a,b]}} {\varphi_2},\; \mathsf{B} \in \{ \mathsf{sU},\overline{\mathsf{sU}} \},\; \lnot P(\varphi,u) \} \\ &\cup \bigcup\limits_{\varphi \in \Gamma(u)} \{ (l+a, r+b) \mid (l,r) \in \mathcal{T}(\varphi_1),\; \varphi = {\varphi_2} \mathbin{{\mathsf{B}}^{{}}_{[a,b]}} {\varphi_1},\; \mathsf{B} \in \{ \mathsf{sR},\overline{\mathsf{sR}} \},\; \lnot P(\varphi,u) \} \\ &\cup \{ (t(u),t(u)) \mid \varphi \in \Gamma(u),\; \varphi = f(R)\bowtie k \lor \varphi = \neg(f(R)\bowtie k),\; \lnot P(\varphi,u) \}. \end{align}\]

If an interval in \(M(u)\) intersects one in \(S(u)\), then we cannot determine when the invariant stops conflicting with the target. Since the extraction might be satisfiable at the next instant, we perform a STEP, and disable the JUMP rule whenever: \[\label{eq:complete-condition} \exists m \in M(u), \exists s \in S(u) \text{ s.t. } m \cap s \neq \emptyset\tag{6}\]

If no such intersection exists, then for every \(m=(l_m,r_m)\in M(u)\) and \(s=(l_s,r_s)\in S(u)\), either \(r_m<l_s\) or \(r_s<l_m\). Case \(r_s < l_m\) is always safe, as the invariant interval is before the target one, and delaying extraction would move the latter to the future. Otherwise, when \(r_m < l_s\), if the target is extracted at time \(t(u)+j\) with \(1 \leq j < k\), its interval becomes \((l_m+j,r_m+j)\). We define the completeness limit as the distance to the earliest time in which the target intervals may appear together with the invariant ones: \[\begin{align} k^{\ast}_{\text{comp}}(u) = \min\big(\{ l_s - r_m \mid (m, s) \in M(u) \times S(u) \land r_m < l_s \} \cup \{ +\infty \}\big). \end{align}\]

4.3.2 Rule Application↩︎

Let \(u\) be a poised node that satisfies both conditions 5 and 6 . The JUMP rule creates one child \(u'\) with \(t(u') = t(u) + k^{\ast}(u)\), where the final jump size \(k^{\ast}(u)\) is defined as \[k^{\ast}(u) = \min(k(u), k^{\ast}_{\text{sound}}(u), k^{\ast}_{\text{comp}}(u))\] and the node label \[\begin{align} \Gamma(u')= &\{ {\varphi_1} \mathbin{{\mathsf{sU}}^{}_{[a,b]}} {\varphi_2}\mid {\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{I}} {\varphi_2}\in\Gamma(u), \; \mathsf{B}\in\{ \mathsf{sU},\overline{\mathsf{sU}} \}, \;t(u') \leq b \}\tag{7}\\ &\cup\{ {\varphi_1} \mathbin{{\mathsf{sR}}^{\psi}_{[a,b]}} {\varphi_2} \mid \varphi = {\varphi_1} \mathbin{{\mathsf{B}}^{{\psi}}_{I}} {\varphi_2}\in\Gamma(u), \;\mathsf{B}\in\{ \mathsf{sR},\overline{\mathsf{sR}} \}, t(u') \leq b \}\tag{8} \end{align}\]

The label \(\Gamma(u')\) omits real-valued constraints and unmarks operators, so that expansion rules can build nodes for the next time instants. Bounds \(k^{\ast}_{\text{sound}}(u)\) and \(k^{\ast}_{\text{comp}}(u)\) guarantee that the JUMP rule preserves remaining temporal obligations while avoiding redundant checks.

Let us evaluate the JUMP bounds on node \(u_2\) in the example of Fig. 1. We have \(k(u_2) = 4\); for the soundness limit, we have \(N(u_2) = \{ (0,0) \}\) and \(O(u_2) = \{ (0,4), (4,6), (4,7) \}\), so \(k^{\ast}_{\text{sound}}(u_2) = 4\); for the completeness limit, we have \(M(u_2) = \{ (0,0) \}\) and \(S(u_2) = \{ (0,4), (4,7) \}\), so \(k^{\ast}_{\text{comp}}(u_2) = 4\). Hence, the JUMP rule can be applied with a jump size of 4, skipping time instants 1 to 3 without losing soundness or completeness.

4.3.3 Correctness↩︎

We prove the soundness and completeness of the JUMP rule by showing, respectively, that an accepted branch in the tableau with it implies an accepted branch in the basic tableau, and vice versa. We report the proofs in Appendix 9.

5 STLSat Tool↩︎

STLSat is a modular tool for satisfiability checking of bounded discrete-time STL formulas. The full implementation, including source code, benchmarks, and reproducibility scripts, is publicly available¹. Given a formula \(\varphi\), STLSat determines whether there exists a discrete-time signal \(w: \mathbb{N} \to \mathbb{R}^n\) such that \((w, 0) \models \varphi\). STLSat implements three different solving engines working over the same formula representation:

• the tableau-based method described in §4;

• a FOL engine for STL inspired by [25];

• a quantifier-free encoding inspired by MPC [19] and bounded model checking [29] methods.

5.1 Tableau Method↩︎

STLSat features an efficient implementation of the tableau methodology described in §4.

It introduces a lightweight syntactic simplification phase before tableau construction. This pre-processing step applies common rewriting rules, including nested conjunction and disjunction flattening, redundant operand removal (e.g., \(\varphi \land \top \equiv \varphi\)), and merging of temporal operator intervals (e.g., \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[0,3]}}\varphi \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[2,5]}}\varphi \equiv \mathop{\mathsf{\mathsf{G}}^{{}}_{[0,5]}}\varphi\)). These simplifications reduce formula complexity and, consequently, the depth of tableau expansion without affecting satisfiability.

Furthermore, STLSat replaces the tableau expansion of [10], which relies on the program call stack for node exploration, with an explicit stack-based implementation. This design enables finer control over memory allocation and improves performance when exploring deep tableaux.

STLSat performs local consistency checks of atomic propositions by invoking the Z3 solver [30]. We also implemented a custom solver for systems of difference constraints through their reduction to negative-cycle detection in graphs [31]–[33]. This optimization improves performance by eliminating the external Z3 calls for supported formulas.

5.1.0.1 Unsat-Core Extraction

Whenever a formula is determined to be unsatisfiable, STLSat performs a lightweight unsatisfiable-core extraction to identify the source of inconsistency. We represent the input formula \(\varphi\) as a conjunction of subformulas after repeatedly applying the \(\land\)-expansion rule, so that at the root node \(u_0\) we have \(\Gamma(u_0) = \{ \varphi_1, \dots \varphi_m \},\) and \(\varphi = \bigwedge_{i=0}^m \varphi_i\). Let \(\mathcal{A}\) be the set of atomic predicates \(f(R)\bowtie k\) occurring in \(\varphi\). We associate each atomic predicate \(a \in \mathcal{A}\) to its originating subformula \(\varphi_i\) through a mapping \(M: \mathcal{A} \to \{ 1, \dots, m \}\).

During tableau expansion, every node contains a set of atomic predicates \(A(u) \subseteq \mathcal{A}\) extracted from the input formula \(\varphi\). When a node is rejected by the underlying theory solver, the solver provides the subset of conflicting atomic predicates responsible for the inconsistency: \[C_u = \{ a_{u,1}, a_{u,2}, \dots, a_{u,k} \} \subseteq A(u).\]

When all branches of the tableau are rejected, the local unsatisfiable cores are aggregated into a single set \(C = \bigcup_{u\text{ rejected}} C_u\) and mapped back to their originating formulas in the root node, producing a high-level unsatisfiable core \(U \subseteq \Gamma(u_0)\) that identifies a subset of subformulas responsible for the inconsistency, with \(U = \{ \varphi_i \mid \exists a \in C : M(a) = i \}.\)

5.2 First-Order Logic Encoding↩︎

An almost out-of-the-box solution for STL satisfiability is to translate a formula \(\varphi\) into First-Order Logic (FOL) by recursively replacing each operator with its semantics definition, and then check the resulting formula with a theorem prover or an SMT solver with quantifier support.

[25] applies this idea to MLTL. They encode signals as functions from integers (representing time) to Boolean values: for each atomic proposition \(p\), they define a function \(p : \mathbb{N} \rightarrow \{\top, \bot\}\), such that \(p(t) = \top\) iff \(p\) holds at time \(t\). Moreover, they define a Boolean function \(f\) taking two integers \(k\) and \(\mathit{len}\), which returns \(\top\) iff the FOL translation of \(\varphi\) is true at time \(k\) for a signal of length \(\mathit{len}\).

We implement an optimized STL encoding where signals are integer‑to‑real functions (for real values) or integer‑to‑Boolean functions (for Boolean signals). The translation follows the semantics in §3. To reduce formula size, we employ the usual ad hoc FOL translations for the \(\mathsf{F}{}\) and \(\mathsf{G}{}\) operators, rather than translating them to \(\mathsf{U}{}\).

5.3 Quantifier-Free SMT Encoding↩︎

Closely related to the FOL approach, STL satisfiability can also be encoded as a quantifier-free SMT problem over linear real arithmetic, similarly to SMT encodings used for optimal control [19] and bounded model checking [29].

The encoding first computes the formula horizon and creates symbolic variables for each signal variable at every time instant. The encoding recursively unfolds the semantics of STL operators. Boolean operators are translated directly into their SMT counterparts, while temporal operators are expanded over their intervals. The resulting quantifier-free linear real arithmetic formula can be solved by an SMT solver.

6 Experiments↩︎

We compare the three engines implemented within STLSat with state-of-the-art tools for STL and MLTL satisfiability. We compare them on both STL and MLTL formulas with STLTree [34], the original Python implementation of the tree-shaped tableau by [10]. We also compare with the best-performing technique for MLTL satisfiability analyzed by [25], namely their FOL encoding which we call MLTLSAT, obtained by running the tool made available by the authors [9]. MLTLSAT translates MLTL formulas into SMTLIB files, which we feed to Z3 4.15.8 [30]. We ran all experiments on a server equipped with an AMD EPYC 9654 CPU and 755 GB of RAM running Ubuntu 24.04.

6.1 Benchmarks↩︎

We evaluate STLSat on two complementary benchmark suites. Table 2 presents descriptive statistics about the temporal formulas used in the evaluation.

MLTL. The first benchmark suite in [25] contains three subsets of MLTL formulas:

• NASA‑Boeing: 63 formulas extracted from real-world avionics systems;

• Random: 4,000 randomly generated formulas with realistic patterns and random integer time intervals;

• Random0: 4,000 randomly generated formulas whose time intervals all start at 0.

All formulas involve only Boolean variables, thus stressing temporal operators over large horizons while abstracting away linear real‑arithmetic reasoning.

STL. The second benchmark suite comprises three groups of STL formulas:

• nine requirements collected by [10] plus the running example 1 ;

• Random‑STL: 2,000 randomly generated formulas of varying length;

• Random0‑STL: 2,000 random formulas of varying length with all intervals starting at 0.

The generation process for the random STL benchmark suites is detailed in Appendix 10.

6.2 Results↩︎

MLTL We compare STLSat with STLTree and the FOL encoding of [25] (MLTLSAT). We show the results as survival plots in Fig. 2, with a timeout of 120 s. Furthermore, we present in Table 3 the number of instances in which each STLSat solving engine was strictly the fastest, grouped by benchmark and formula satisfiability for both MLTL and STL suites. On the NASA-Boeing suite the FOL encoding (§ 5.2) dominates: it solved 62 benchmarks within 80 s, launching a parsing error on 1, while MLTLSAT solved 46 benchmarks within 108 s and timed out on 14 launching parsing errors on 3. This advantage comes from a smaller generated encoding with fewer quantifiers: these formulas—derived from manually written requirement sets—contain only \(\mathsf{F}{}\) and \(\mathsf{G}{}\) rather than \(\mathsf{U}{}\) operators, and can benefit from our ad hoc encoding of \(\mathsf{F}{}\) and \(\mathsf{G}{}\).

On the other hand, tableau-based tools perform better on randomly generated formulas, with STLSat outperforming STLTree despite using stricter jumping rules, thanks to the efficient algorithm implementation. In fact, formulas in these suites contain many temporal operators with wide time intervals, which can greatly benefit from the tableau’s JUMP rule. The SMT encoding (§ 5.3) is the worst in all benchmarks, consistently with the findings of [10].

Executing STLSat’s three solving engines in parallel brings a slight benefit in random benchmarks, because there are some formulas for which one particular engine performs better than the others. In the NASA-Boeing set, instead, the FOL encoding terminates first on the large majority of instances (although with very low margin), and parallel execution discounts the overhead of running all engines.

STL Table 4 shows our comparison on benchmarks from [10], plus the running example 1 . STLSat outperforms STLTree in some benchmarks, but times out in the largest ones; on the other hand, the FOL encoding quickly solves CPS, and the SMT encoding solves Aerospace without timing out.

Fig. 3 shows survival plots for randomly generated STL formulas. STLSat’s tableau performs slightly worse than STLTree, but much better than the FOL and SMT encodings. Table 3 suggests that the tableau is the fastest engine on most instances, while FOL and SMT are each fastest on smaller subsets of formulas. Namely, FOL wins on most of the NASA-Boeing benchmarks, and wins more frequently in unsatisfiable instances than satisfiable ones. Consequently, parallel execution of the STLSat engines yields further computational gains.

7 Conclusions↩︎

We present STLSat, an open‑source Rust tool that efficiently decides the satisfiability of bounded discrete‑time STL formulas. We uncovered an unsound optimisation in the tableau introduced by [10] and replaced it with a sound, complete rule. In addition to the tableau, STLSat offers two alternative encodings: a first‑order-logic translation and a quantifier‑free SMT encoding for linear real arithmetic. All three engines can be executed in parallel as a portfolio solver.

Our extensive benchmark suite (covering both STL and MLTL, with real‑world and randomly generated instances) shows that STLSat performs comparably to STLTree, and often outperforms state-of-the-art tools such as MLTLSAT, and standard SMT encodings. Furthermore, running all STLSat solving engines in parallel yields the best overall performance. Moreover, unsatisfiable‑core extraction facilitates specification mining, redundancy elimination, and traceability in CPS development.

Future work will focus on temporal analysis for unsat cores, support for unbounded STL operators and continuous‑time semantics, tighter integration with model‑checking, falsification, and specification mining, and the development of visual debugging interfaces that display counterexample signals and core constraints.

Acknowledgements↩︎

Partially funded by the European Union. Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Health and Digital Executive Agency (HADEA). Neither the European Union nor the granting authority can be held responsible for them. RobustifAI project, ID 101212818; VASSAL project, ID 101160022.

8 Flaws in the \(\mathsf{JUMP}_\mathsf{O}\) rule↩︎

In this section, we show that the \(\mathsf{JUMP}_\mathsf{O}\) rule by [10] undermines both soundness and completeness of the tableau. We report the definition of the \(\mathsf{JUMP}_\mathsf{O}\) rule almost verbatim from [10] below.

[10] manage formula superscripts in a slightly different way: nested operators extracted by expansion rules are annotated with the interval of the parent formula, rather than the formula itself: \[\begin{align} &\operatorname{tex}^t_I({\varphi_1} \mathbin{{\mathsf{B}}^{{}}_{[a,b]}} {\varphi_2}) = {\varphi_1} \mathbin{{\mathsf{B}}^{{I}}_{[a+t,b+t]}} {\varphi_2} && \text{with } \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \} \end{align}\] where \(I\) is the interval \([a,b]\) in Table 1, and \(\operatorname{tex}^t_I\) substitutes \(\operatorname{tex}^t_\psi\) in that table. Note that, since such superscripts are not used in the basic tableau, this change does not interfere with its correctness.

The \(\mathsf{JUMP}_\mathsf{O}\) rule can be applied to a poised node \(u\) if all marked operators \({\varphi_1} \mathbin{{\overline{\mathsf{sU}}}^{J}_{[a,b]}} {\varphi_2}\) or \({\varphi_2} \mathbin{{\overline{\mathsf{sR}}}^{J}_{[a,b]}} {\varphi_1}\) in \(\Gamma(u)\), with \(J = [a_J, b_J]\) and \(t(u) \geq b_J\), are such that

1. \(t(u) < b\), and

2. for all temporal operators \(\psi\) in \(\varphi_1\) that are not nested in any other temporal operator we have \(t(u) \geq a + I_u(\psi)\),

where \(I_u(\psi)\) is the upper bound of \(\psi's\) time interval (e.g., \(I_u(\mathop{\mathsf{\mathsf{G}}^{{}}_{[a,b]}}\psi') = b\)). Otherwise, only the STEP rule can be applied.

If the conditions above are met, then \(u\) has one child \(u'\) such that \(t(u') = \min \{ t \in K(u) \mid t > t(u) \}\), where \[K(u) = \{ a, b \mid {\varphi_1} \mathbin{{\mathsf{B}}^{{J}}_{[a,b]}} {\varphi_2} \in \Gamma(u) \land \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR}, \overline{\mathsf{sU}}, \overline{\mathsf{sR}} \} \land t(u) \geq b_J \},\] and, setting \(k = t(u') - t(u)\), we have \[\begin{align} \Gamma(u') = &\;\{ {\varphi_1} \mathbin{{\mathsf{B}}^{{J}}_{I}} {\varphi_2} \in \Gamma(u) \mid \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \} \land t(u) \geq b_J \} \\ &\cup \{ {\varphi_1} \mathbin{{\mathsf{B}}^{{J}}_{[a+k, b+k]}} {\varphi_2} \mid {\varphi_1} \mathbin{{\mathsf{B}}^{{J}}_{[a,b]}} {\varphi_2} \in \Gamma(u) \land \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \} \land t(u) < b_J \} \\ &\cup \{ {\varphi_1} \mathbin{{\mathsf{B}}^{{J}}_{[a,b]}} {\varphi_2} \mid {\varphi_1} \mathbin{{\overline{\mathsf{B}}}^{J}_{[a,b]}} {\varphi_2} \in \Gamma(u) \land \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \} \land t(u) \geq b_J \land t(u) < b \} \\ &\cup \{ {\varphi_1} \mathbin{{\mathsf{B}}^{{J}}_{[a+k,b+k]}} {\varphi_2} \mid {\varphi_1} \mathbin{{\overline{\mathsf{B}}}^{J}_{[a,b]}} {\varphi_2} \in \Gamma(u) \land \mathsf{B} \in \{ \mathsf{sU}, \mathsf{sR} \} \land t(u) < b_J \land t(u) < b \} \end{align}\]

The \(\mathsf{JUMP}_\mathsf{O}\) rule has two main issues:

1. requirement [item:oldjump-pcl-rule] only takes into account one level of nesting of temporal operators, and only in the right-hand-side operand; and

2. the set \(\Gamma(u')\) does not faithfully re-create the label that node \(u'\) would have if it had been reached by repeatedly applying the STEP rule until reaching a node with \(t = t(u) + k\), dropping formulas that can reveal inconsistencies.

As briefly shown in Section 4.2, the formula \(\varphi_S\), which we repeat here for convenience, witnesses the unsoundness of this rule: \[\varphi_S = {(\mathop{\mathsf{\mathsf{G}}^{{}}_{[0,0]}} \mathop{\mathsf{\mathsf{G}}^{{}}_{[5,5]}} a)} \mathbin{{\mathsf{sU}}^{}_{[0,4]}} {(\mathop{\mathsf{\mathsf{G}}^{{}}_{[5,5]}} \neg c)} \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[5,8]}} c \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} \neg a\]

Figure 4 shows part of the tableau rooted in \(\varphi_S\) that uses the \(\mathsf{JUMP}_\mathsf{O}\) rule. First, the tableau tries to satisfy the \(\mathsf{U}\) operator at time 0 by expanding it to \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[5,5]}} \neg c\) in node \(u_2\), but this leads to a contradiction with \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[5,8]}} c\). It thus tries extracting \(\psi = \mathop{\mathsf{\mathsf{G}}^{{}}_{[0,0]}} \mathop{\mathsf{\mathsf{G}}^{{}}_{[5,5]}} a\) in node \(u_3\), and since here \(I_u(\psi) = 0\), the conditions for the \(\mathsf{JUMP}_\mathsf{O}\) rule apply. Thus, the tableau jumps to \(u_8\) which, as noted in Section 4.2, does not contain \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} \neg c\), allowing the satisfaction of all operators.

The new JUMP rule that we present in Section 4.3 does not incur in the same issue thanks to the soundness limit (cf.Section 4.3.1). In fact, due to the \(\mathsf{U}\) operator we have \((0,5) \in N(u)\) and due to \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} \neg a\) we have \((8,8) \in O(u)\). Thus, we have \(k^{\ast}_{\text{sound}}(u) \leq l_o - r_n = 8 - 5 = 3\): the tableau may jump at most to a node \(u'\) with \(t(u') = 3\), in which either we try to satisfy the \(\mathsf{U}\) operator, incurring in the contradiction between \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} \neg c\) and \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[5,8]}} c\), or we postpone its satisfaction, revealing the contradiction between \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[3,3]}} \mathop{\mathsf{\mathsf{G}}^{{}}_{[5,5]}} a\) and \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[8,8]}} \neg a\).

The \(\mathsf{JUMP}_\mathsf{O}\) rule also undermines the completeness of the tableau. Consider the following formula: \[\varphi_C = {a} \mathbin{{\mathsf{sU}}^{}_{[0, 10]}} {(b \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[20, 30]}} c)} \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[0, 27]}} \neg c \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[10, 10]}} \neg b\] This formula is satisfiable, as shown by an accepting branch of the basic tableau in Figure 5. In satisfying signals, the \(\mathsf{sU}\) operator must have its right-hand-side satisfied at times 8 or 9. In fact, formula \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[20, 30]}} c\) conflicts with \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[0, 27]}} \neg c\) if it is extracted at a time in between 0 and 7, while \(b\) conflicts with \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[10, 10]}} \neg b\) at time 10.

Thus, the tableau branch that tries to satisfy the \(\mathsf{sU}\) operator at time 0 is rejected, while the one that postpones its satisfaction remains. The \(\mathsf{JUMP}_\mathsf{O}\) rule then jumps directly to time 10, where the \(\mathsf{sU}\) operator must be satisfied, but it cannot: by skipping nodes with times 8 and 9, the \(\mathsf{JUMP}_\mathsf{O}\) rule prevents the tableau from finding two possible accepting branches. Thus, the \(\mathsf{JUMP}_\mathsf{O}\) rule makes the tableau incomplete, as it may declare unsatisfiable formulas that are actually satisfiable.

On the contrary, with our JUMP rule, in each node \(u\) with \({a} \mathbin{{\mathsf{sU}}^{}_{[0, 10]}} {(b \land \mathop{\mathsf{\mathsf{G}}^{{}}_{[20, 30]}} c)} \in \Gamma(u)\) we have \((t(u)+20, t(u)+30) \in M(u)\), and \((0,27) \in S(u)\), due to \(\mathop{\mathsf{\mathsf{G}}^{{}}_{[0, 27]}} \neg c\). Since for all \(t \in [0,7]\) we have \((t+20, t+30) \cap (0,27) \neq \emptyset\), the JUMP rule cannot be triggered until a node with time 8 is reached. In such a node the expansion rule for the \(\mathsf{sU}\) operator is applied, generating an accepting branch.

9 Theorem Proofs↩︎

10 Random Benchmark Generation↩︎

The Random-STL and Random0-STL benchmark suites were generated using a stochastic recursive expansion algorithm. The generator is implemented in Rust using the set of functions provided by the formula module of the STLSat tool.

10.1 Generation Algorithm↩︎

The generator constructs formulas as conjunctions of \(j\) independently generated sub-formulas. Each of these formulas is produced by a recursive function.

10.1.0.1 Recursive Generation

The generation of a branch is terminated once an atomic proposition is selected (as it has no children). The average formula depth is controlled by a parameter \(p_{\text{stop\_base}}\), representing the probability of selecting an atomic proposition. This probability grows linearly with the current tree depth \(d\) such that \(P_\text{stop} = \min(1.0, p_{\text{stop\_base}} \times d)\).

10.1.0.2 Temporal Operator

Whenever the recursion continues, the algorithm selects between a temporal or a non-temporal operator based on a parameter \(p_{\text{temp}}\). Whenever a temporal operator is selected, the operator is chosen uniformly from the set \(\{ \mathop{\mathsf{\mathsf{F}}^{{}}_{,}} \mathop{\mathsf{\mathsf{G}}^{{}}_{,}} \mathsf{U}, \mathsf{R} \}\). The corresponding interval \(I = [a,b]\) is computed to ensure the global temporal horizon is not exceeded. Let \(h\) denote the current accumulated horizon at the given tree depth, \(l\) the maximum global horizon parameter, and \(i\) the maximum allowable interval length parameter. The maximum permissible time interval length is \(\Delta_{\max} = \min(i, l - h)\).

For the Random-STL benchmark, the interval \(I\) is generated by selecting one of three modes with equal probability:

• \(a = 0\), and \(b \sim \mathcal{U}(0, \Delta_{\max})\).

• \(a \sim \mathcal{U}(0, \Delta_{\max})\), and \(b \sim \mathcal{U}(a, \Delta_{\max})\).

• \(a \sim \mathcal{U}(0, \Delta_{\max})\), and \(b = l - h\).

For the Random0-STL benchmark, the generation enforces the first mode (with \(a = 0\) for all temporal operators).

10.1.0.3 Atomic Proposition

When an atomic proposition is selected, it is sampled from a pre-generated pool of \(c\) constraints. These constraints operate over the real variables \(S = \{x_1, \dots, x_r\}\) and can take three forms, which are selected uniformly:

1. Simple Bounds: \(x_i \bowtie k\).

2. Difference Logic: \(x_i - x_j \bowtie k\) for \(i \neq j\).

3. Linear Constraints: \(\sum_{x \in S'} x \bowtie k\), where \(S' \subseteq S\) is a randomly selected subset.

The relation \(\bowtie\) is sampled from \(\{<, \leq, >, \geq, =, \neq\}\), while the constant \(k\) is a randomly generated rational number.

10.2 Parameter Space and Suite Configuration↩︎

The Random-STL suite was generated by sweeping across all combinations of the parameter space. Table 5 presents the set of possible parameter values for each defined parameter. For each combination of parameters, \(5\) formulas have been generated, for a total of \(2000\) formulas. The Random0-STL variation uses identical parameter space value combinations but restricts all generated temporal operator intervals to the form \([0, b]\), as detailed in the previous section.

References↩︎

---

1. https://github.com/ZamponiMarco/stlsat/↩︎

2. We assume \(\varphi\) to be in strict normal form, so temporal operators cannot be nested in a negation.↩︎

3. More precisely, here we apply to \(\theta\) a variant of the proof of Lemma 1 in which only the \(\theta_1\) operand of \(\theta\) is considered.↩︎