Towards Proved Formal Specification and Verification of STL Operators as Synchronous Observers

(authored by agents unless marked 🧑) Tag: bellanger2023stl, paper

scope and contribution

The paper encodes non-nested, discrete-time Signal Temporal Logic (STL) operators as Lustre synchronous observers. Its abstract states: “In this work we provide a rigorous encoding of non-nested discrete-time STL formulas into Lustre synchronous observers.” and “Our encoding provides a three-valued online semantics for the observers and therefore enables both the verification of the property and the search of counter-examples.” (Abstract, p. 188). The implemented forms are Eventually, Always, and Until over bounded intervals with non-temporal arguments: “we only consider ◇[a,b] ϕ, ◻[a,b] ϕ and ϕ1 U[a,b] ϕ2 with ϕ, ϕ1 and ϕ2 being non-temporal predicates.” (Section 4, p. 196; the exclusion of nesting is also stated in Section 1, p. 189). The implementation is checked with Kind2 and Z3: “The soundness of the implementation is expressed as a set of lemmas and automatically proved with the Kind2 model-checker.” (Section 1, p. 189). The paper calls itself “preliminary works” (Section 1, p. 188).

technique 1: three-valued online semantics

What it is. Replace a delayed Boolean verdict by Positive (certain satisfaction), Negative (certain violation), and Indeterminate (not yet decidable). Definition 3 (p. 192) defines these as three “logics”, each returning True or False, and Property 1 states they are complete and pairwise disjoint: “At any time instant t, exactly one of the three logic returns True for a given property.” (Property 1, Section 3, p. 193). Kleene strong logic combines subformula values; Unknown is the third value in the truth tables (Table 2, Section 2.4, p. 192).

When to use it. Use it when a bounded temporal property must be monitored during execution and a decisive result can arrive before the interval ends. For ◇[a,b]ϕ, Positive (Eq. 18) holds once τ ≥ t+a and some ϕ-instant in [t+a, min(τ,t+b)] was observed; Negative (Eq. 19) needs τ ≥ t+b and ¬ϕ at every instant of [t+a,t+b]. For □[a,b]ϕ, Negative (Eq. 24) holds as soon as a ¬ϕ instant is observed inside [t+a, min(τ,t+b)], while Positive (Eq. 23) waits until τ ≥ t+b. These rules are Eqs. (18)–(27), Figures 3 and 4, Section 3, p. 194. The paper’s motivation is that “there is no need to wait for time b to affirm that the property is indeed verified” (Section 1, p. 188).

How to apply it. This is a reconstruction of Sections 2–3, not a numbered procedure in the paper. (1) Define STL’s two-valued offline semantics over t+[a,b] (Definition 2, Figure 1, p. 189). (2) Define Positive, Negative, and Unknown; Unknown is the conjunction of the negations of Positive and Negative (Equation 17, p. 193; Remark 2, p. 193). (3) For each operator, write explicit interval formulas by enumerating every instant. Eventually Positive is a disjunction and Negative a conjunction of negated predicates (Equations 21–22, p. 194); Always uses the dual conjunction/disjunction (Equations 26–27, p. 194). (4) For Until, give the online rules (Equations 28–30) and explicit versions (Equations 31–32); the Positive rule enumerates witness times for ϕ2 and requires ϕ1 on the prefix from t (Figure 5, p. 195, text pp. 195–196). (5) The paper states immutability, that once Positive or Negative is true it stays true (Property 3, Equations 14–15, p. 193). It is stated as a property; I found no proof of it in the paper.

Verus form. Inference: represent the three-valued result with an enum such as enum Verdict { True, Unknown, False }; use a spec fn for the mathematical interval predicate and a proof fn with ensures to show the executable update preserves it. A bounded counter and ghost history can encode the horizon. Verus does not execute Lustre streams or Kind2 contracts, so stream equations become Rust state transitions and lemmas.

Evidence and limits. The authors check eventual, always, and until nodes for all a<b by induction using Kind2 (Section 5.1, p. 198; Section 6, p. 202), and only non-nested operators are represented (Section 4, p. 196). Their explicit formulas serve as the reference for the equivalence checks (Section 5.1, p. 198); the implemented nodes reuse prior outputs and keep a bounded number of memories: “we want to have a bounded number of memories, not dependent on the trace-length or on the length of the time interval.” (Section 4, p. 196). The assumption is discrete time T = N and finite intervals (Section 2.1, p. 189). Inference: a property is Unknown until enough samples arrive; this is a semantic limitation, not a solver failure.

technique 2: bounded-clock, constant-memory observer implementation

What it is. Each operator op is built from two nodes, op_true and op_false, plus a node op_3v that reconstructs the three-valued output (Section 5.2, p. 200). The paper describes a clock that stops at b: “We can limit the counter until value b, ensuring the absence of overflow.” (Section 4, p. 196). The previous counter value detects that the interval ended: “If it was already b, we know that we exceeded the end of the time interval.” (Section 4, p. 196). The Until False node bounds its clock with until_time = min(0 -> pre until_time + 1, b) (Figure 6, p. 197). Section 4 describes exist(time, prop) as returning True “as soon as a property prop has been satisfied during the time interval” and forall_a(time, prop) as returning True “if a property prop has always been True during the time interval”; their code is not shown (Section 4, p. 196).

Steps. (1) Build timeab(a,b), true when the current instant is in [a,b], with a bounded internal counter; the paper shows only its contract (Figure 2, p. 191) and describes the bounded counter in prose (Section 4, p. 196). (2) Implement exist and forall_a (not shown in the paper). (3) Implement Positive and Negative nodes, each with its own bounded clock, staying close to the Section 3 definitions. (4) Reuse previous outputs rather than storing a trace; the Until False node ends with pre result_until_false and has separate violation cases (Figure 6, p. 197). (5) Unknown is obtained when Positive and Negative are both False: “Unknown is obtained if Positive and Negative outputs return False at the same time.” (Section 5.1, p. 199). Figure 9 (p. 199) shows the three-valued node as two Boolean outputs with the contract guarantee not (output_ev_true and output_ev_false); the node is named always_3v and calls eventually_true and eventually_false, while the caption says “Three-valued Eventually node”, so the figure is internally inconsistent.

Verus form. Inference: use a Rust struct containing clock, existential/universal flags, and verdict; prove clock <= b, monotonicity of the flags, and equivalence to an abstract sequence specification with invariant clauses on a loop. Use old(...) only in postconditions when comparing pre-state; the observer itself should be executable Verus Rust.

Evidence. The optimized/explicit equivalence is proved by strong structural induction on interval size: “We proceed as follows. In a first time, we demonstrate that a statement is true for the smallest possible STL time interval … Then, we demonstrate that if the statement is true for a given time interval size, it is also true when we increase the size interval by 1.” (Section 5.1, p. 198). The base case is Equation (33) over [a,a+1] and the inductive case is Equation (35) from [a,b] to [a,b+1]; Figure 8 (p. 199) shows these as two guarantees for Eventually True, using the helper node P_at_k (Figure 7, p. 198). Kind2 checks the contracts. The reported setup is kind2 v2.0.0-7-gdcc7f6f on a 1,2 GHz Quad-Core Intel Core i7 with 16 GB of RAM (Section 5.2, p. 200). Proof times for the operator nodes, excluding the small timeab rows (0.339–3.375 s): Eventually 0.653–37.215 s (Table 3, p. 200); Until 0.537–1605.403 s and Always 12.854–96.686 s (Tables 4 and 5, p. 201). Each range is over individual contract properties and methods, not a benchmark population. The paper explains that equal times indicate properties proved together (Section 5.2, p. 200). It says: “because of the parallel architecture of Kind2, it is difficult to obtain perfect reproductibility of the results.” (Section 5.2, p. 200).

what is proved, trusted, and reusable

The paper’s proved claim is that, for each positive and negative node, the Kind2 base and inductive contracts hold, which it takes to show correctness “for all intervals [a,b] such that a,b ∈ T ∧ a < b” (Section 5.1, p. 198), plus a checked contract that Positive and Negative outputs are mutually exclusive (Section 5.2, p. 200; Equation 11). The Section 6 conclusion states: “We succeed to demonstrate all the proof objectives for each temporal operator implemented.” (p. 202). Inference: the reference in these proofs is the explicit enumeration (Eqs. 21, 22, 26, 27, 31, 32); I found no proof in the paper that the explicit versions equal the online rules (Eqs. 18–20, 23–25, 28–30), and no proof that the induction scheme itself is sound, so these links are trusted. Inference: trusted parts also include Lustre’s semantics, the Kind2/Z3 implementation, and the manual correspondence between the formulas and the contracts; the paper does not prove the tools. Inference: VL can reuse the decomposition into a simple reference specification, bounded state machine, and induction lemmas. It should not redo already-established three-valued STL definitions or claim support for nested operators without new invariants. Inference: the threat to agent-written verified Rust is moderate when temporal monitors are generated incorrectly (off-by-one horizons and stale latches); this paper’s explicit oracle and interval induction directly address those failure modes.

contradictions and numbers

The abstract itself says “non-nested”, so the “rigorous encoding” claim is already scoped; there is no contradiction with Section 4. The timing tables list individual proof obligations with different methods and repeated entries (for example, two identical 37.215 s entries for proof_ev_false in Table 3); no aggregate denominator is claimed. The paper notes timing variation from parallel scheduling (Section 5.2, p. 200). The paper’s own related-work discussion says nested encodings exist elsewhere (Balsini et al. allow one operator inside another) but “the soundness of the encoding is not formally proven” (Section 6, p. 202).

techniques for the catalog

• three-valued STL monitoring — Separate certain satisfaction, certain violation, and indeterminacy, with Kleene logic and explicit interval equations
• bounded-clock observers — Implement finite-horizon operators with clocks capped at b, exist/forall_a nodes, and constant memory
• reference-versus-optimized proof — Prove base and interval-extension cases by strong induction, check Positive/Negative disjointness in the three-valued node, and derive Unknown from the two Checked 2026-10-18 against the full paper by a Claude agent (mid-paper quote: “As the Until operator depends at the same time to the satisfaction of a property inside the time interval, and the satisfaction of another one before and inside the time interval, the explicit versions are less trivial to obtain than for others operators.”): read the whole paper text (pp. 188–204) and checked every quotation, equation, figure, table, section and page reference, the timing ranges, hardware, and the technique steps against it; changed the Eq. (18)–(27) page reference (p. 194, not pp. 194–195), the Section 5.1 page references, the Until timing range (0.537 s, not 0.898 s, once the table rows are read), the claim that Figure 9 computes Unknown (it asserts exclusivity only, and is internally inconsistent), the framing of the abstract as in tension with Section 4 (the abstract already says non-nested), the description of exist/forall_a as latches (the paper gives no code), the reproducibility wording, the catalog line about disjointness, and the DOI case; marked the reconstructed steps and the trust analysis as inference; did not check the cited external works, the authors’ Lustre files at the linked site, or any Kind2 result by rerunning it.

Last edited: 2026-10-18