Pith. sign in

REVIEW 5 minor 27 references

Semantics for Linear-time Temporal Logic with Finite Observations

T0 review · 0 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper gives LTL3, the three-valued temporal logic used in runtime verification, a compositional inductive semantics based on definitive prefix sets, and proves this semantics equivalent to conventional LTL and to the…

desk verdict Definitive-prefix semantics for LTL3 is a real, machine-checked advance; the progression theorem is sound but hinges on a validity oracle the authors openly acknowledge. read the letter →

arxiv 2411.14581 v1 pith:CUDBMZKC submitted 2024-11-21 cs.LO

Rayhana Amjad (University of Edinburgh) , Rob van Glabbeek (University of Edinburgh) , Liam O'Connor (Australian National University) This is my paper · ORCID
classification cs.LO MSC 03B4468Q60
keywords LTL3definitiveprefixsetsruntimeverificationformulaprogressionlinear-timetemporallogicpartialtracesthree-valued
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

LTL3 is the three-valued version of linear-time temporal logic used in runtime verification: a finite observation of a running system can settle a formula as true, false, or still undetermined. Earlier definitions of LTL3 were non-inductive, quantifying over all possible infinite extensions of the observed prefix, and it had been claimed that no inductive, compositional semantics could exist. This paper refutes that claim by assigning to every formula a pair of definitive prefix sets, the traces that already force the formula to true or false, and shows that these sets are completely determined by their infinite traces. It follows that LTL3 is not really a separate logic but a finer-grained presentation of conventional LTL: the infinite traces that the new semantics assigns to true and false are exactly the traces satisfying and falsifying the formula in ordinary LTL. The paper also formalizes formula progression, the standard step-by-step evaluation technique, and proves it sound and complete up to finite traces with respect to this semantics; all definitions and proofs are machine-checked.

What carries the argument

The load-bearing object is the definitive prefix operator $\mathbin{\varobslash}X = \{t \mid \uparrow t \subseteq \downarrow X\}$, which collects all traces whose every extension is a prefix of some trace in $X$; such traces are exactly those from which membership in $X$ cannot be escaped. The definitive sets, those with $X = \mathbin{\varobslash}X$, form a complete lattice under inclusion with a custom definitive union, and the pair of maps $\mathrm{Pr}(X)=X\cap\Sigma^\omega$ and $\mathrm{Df}(P)=\mathbin{\varobslash}P$ forms a lattice isomorphism between definitive sets and linear-time temporal properties. The semantics is given as answer-indexed families $\mathcal{B}\to\mathcal{D}$, with the prepend operation $\triangleright X = \{t \mid t\mid_1\in X\}$ (which preserves definiteness) and an iterative construction for the until operator. This machinery carries the argument by making every formula constructor compositional while keeping the three-valued interpretation: the $T$ and $F$ sets are not complements, and the excluded-middle theorem states each is the definitive closure of the complement of the other.

What would settle it

Brute-force a small finite-state alphabet: enumerate all LTL formulae up to a fixed operator depth and all finite traces up to a fixed length, and compare the paper's inductive semantics with the original definition $[t\models_3\varphi]$. Any finite trace where the two disagree would refute Theorems 6 and 7 as stated; since the proofs are machine-checked, a realistic failure mode would be a transcription error in definitions rather than a flaw in the theorems themselves. For an implementation-level test, run formula progression with only propositional simplifications on the formula $(\ocircle a)\lor(\ocircle\lnot a)$ with the empty trace: the theorem says a semantically trivial formula must result, so any implementation that fails reveals the simplifier assumption in action.

Watch

Extended reading notes

Core claim

The central discovery is an isomorphism between definitive prefix sets and linear-time temporal properties. A definitive prefix set for a set of infinite traces $X$ is the set of all finite or infinite traces every extension of which is a prefix of a trace in $X$; intuitively, these are the observations that already make membership in $X$ inevitable. The paper constructs for each LTL formula $\varphi$ an answer-indexed family $\llbracket\varphi\rrbracket_3$ assigning a definitive set to each truth value, built compositionally with operations for negation, conjunction, disjunction, next, until, and a prepend operation. Theorem 7 states that restricting these definitive sets to infinite traces recovers the standard LTL semantics: $\mathrm{Pr}(\llbracket\varphi\rrbracket_3^T)=\llbracket\varphi\rrbracket^T$ and $\mathrm{Pr}(\llbracket\varphi\rrbracket_3^F)=\llbracket\varphi\rrbracket^F$. Theorem 11 then proves that formula progression is sound and complete up to finite traces: a finite trace $t$ is definitively true for $\varphi$ exactly when progressing $\varphi$ along $t$ reaches a formula whose semantics is the universal set, and symmetrically for false.

Load-bearing premise

The load-bearing premise is that formula progression is interleaved with a simplifier powerful enough to decide whether a progressed formula is semantically trivial (true for all traces or false for all traces); the paper does not construct such a simplifier, so the completeness result is conditional on that oracle.

Editorial extensions

If this is right

  • LTL3 gains no expressive power beyond conventional LTL; any property it can definitively establish or refute from finite prefixes is exactly an ordinary LTL property over infinite traces.
  • Formula progression can serve as an operational semantics for LTL3 on finite traces, with soundness and completeness up to finite traces, so runtime monitors and property-based testers built on progression are formally justified.
  • The definitive-prefix framework gives a uniform way to express good and bad prefixes, monitorability, and the safety/liveness classification, including alternative characterisations of safety and liveness properties.
  • The same answer-indexed family technique is proposed as a foundation for other partial-trace and multi-valued logics, such as RV-LTL, rLTL, and logics with presumptive or probabilistic answers.
  • Because all proofs are machine-checked, the semantics and the progression theorems can serve as a reference specification for implementations.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the isomorphism view is taken seriously, the '?' value of LTL3 is not a third truth value but the absence of a definitive prefix, which suggests redesigning monitors to emit a verdict only when the observed prefix enters a definitive set, rather than at every step.
  • The equivalence theorem implies a monitoring strategy based on conventional LTL automata: checking whether a prefix is definitive reduces to a universal question over all infinite extensions, which can be answered by automata-theoretic emptiness or universality checks.
  • The paper's own example $(\ocircle a)\lor(\ocircle\lnot a)$ shows that propositional simplification is not enough; a natural next step would be to characterize syntactically the class of formulae whose definitive-prefix set is universal, which would turn the 'sufficiently powerful simplifier' assumption into an implementable algorithm.
  • The paper conjectures that its notion of monitorability coincides with the monitor-synthesis notion in modal mu-calculus; if true, syntactic monitorability fragments from that setting could transfer to LTL3, yielding a practical syntactic account of which formulas are monitorable.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. The paper gives a new inductive, model-based semantics for LTL3, the three-valued variant of LTL used in runtime verification. Instead of defining the truth value of a formula on a finite prefix by quantifying over all infinite extensions, it assigns to each formula an answer-indexed family of definitive prefix sets: for each truth value, the set of finite and infinite traces that settle that value. It proves (Theorem 7) that the infinite traces in these sets are exactly the traces satisfying (respectively falsifying) the formula in ordinary LTL, and (Theorem 6) that this coincides with the original extension-based LTL3 definition. It also develops the lattice of definitive sets and shows it is isomorphic to the lattice of linear-time properties. The second half formalizes formula progression as a syntax-directed transition system and proves (Theorems 9–11) that, modulo the ability to recognize formulae with trivial semantics, progression is sound and complete up to finite traces. All definitions and theorems are mechanized in Isabelle/HOL, and the development is available as an Archive of Formal Proofs entry.

Significance. The paper's main semantic results are highly credible because they are machine-checked: the Isabelle/HOL development is public and covers the central theorems. The paper also refutes an earlier claim by Bauer et al. that LTL3 cannot be given an inductive semantics, and it connects definitive prefixes with Kupferman–Vardi good and bad prefixes and with safety/liveness classifications. The progression theorem provides a semantic justification for a widely used runtime-verification technique, although its algorithmic force is limited by the fact that the required notion of 'trivial semantics' is a semantic oracle (equivalently, LTL validity). Overall this is a solid, useful contribution to the semantic foundations of runtime monitoring, with an unusually high level of formal assurance.

minor comments (5)
  1. [5, Theorem 11; abstract and conclusion] The paper explicitly acknowledges that a purely syntactic characterization of the required simplifier is out of scope, but the abstract and conclusion say that the paper 'formalises the formula progression evaluation technique' without this caveat. Please add a sentence making explicit that Theorem 11 establishes soundness and completeness relative to a semantic oracle for triviality, and that by Theorem 7 the condition Jphi'K3 T = Sigma^infty is equivalent to LTL validity, hence PSPACE-complete.
  2. [4.3, Theorem 6] The proof of Theorem 6 is compressed to 'follows directly from the definition of definitive sets.' It would be clearer to spell out the decisive fact that, for a definitive set X, a finite trace t belongs to X exactly when every infinite extension of t belongs to Pr(X), and then cite Theorem 7 for the identification of Pr(JphiK3 T) with JphiK T.
  3. [3.1] The same symbol /⊙◇⊞ is used both for the false formula and for the least definitive set (the empty set). This conflation is convenient but may confuse readers; a sentence distinguishing the formula-level and set-level uses would help.
  4. [5 and 6.1] There are a few typos: in Section 5 the text reads 't is in t is in JphiK3 F', and in Section 6.1 it reads 'it it not ugly'. These should be corrected.
  5. [5, Theorems 9 and 10] The proof sketches for Theorems 9 and 10 refer repeatedly to distributive properties of the prepend operator over intersection and definitive union, but these lemmas are not stated in the paper. Stating them explicitly, or at least giving the exact statements with pointers to the Isabelle formalization, would make the proofs substantially easier to follow.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the inductive LTL3 semantics, definitive-set isomorphism, and formula-progression soundness/completeness are independently defined and machine-checked; the acknowledged simplifier gap is an implementability limitation, not a circular step.

full rationale

The paper contains no fitted parameters, no data fitting, and no prediction that is statistically forced by construction. The core semantic definitions are given explicitly: J·K3 is defined compositionally over definitive prefix sets, conventional LTL semantics is defined separately via satisfaction over infinite traces, and the two are connected by Theorem 7, which is proved by structural induction on formulae using the Pr/Df lattice isomorphism of Theorem 2. The isomorphism itself is proved from the definitions of definitive prefixes and projection, not assumed. Theorem 6, despite its terse proof, compares the new inductive semantics with the original quantifier-based LTL3 definition; the equivalence is a derived theorem, not an input to the definitions. The formula-progression results, Theorems 9-11, are proved by structural induction over formulae and by induction on finite trace length, relating the progression rules of Figure 5 to the independently given model-based semantics. The paper explicitly acknowledges in Section 5 that a purely syntactic characterization of the required simplifier is outside scope and that the development works at the level of model-based semantics. This means Theorem 11 is relative to a semantic oracle and does not by itself establish the implementability of progression-based monitoring, but this is an acknowledged scope limitation, not a circular reduction: the equivalence theorem does not assume the conclusion it proves. The self-citations, [AGO24] for the Isabelle formalization and [OW22] for prior use of progression, are contextual and not load-bearing in any proof. No part of the derivation chain reduces to its own inputs by definition, and no uniqueness theorem or prior claim is imported from the authors to forbid alternatives. Therefore the paper should be scored 0 for circularity.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

This is a pure formal-logic paper with no numeric fitting. The free-parameter ledger is empty. The axioms are the Isabelle/HOL logical foundation, the standard trace model, the standard LTL semantics as benchmark, and the explicit semantic-triviality oracle needed for the formula-progression theorem. The only invented construction, definitive prefix sets with answer-indexed families, is a defined mathematical object rather than an empirical postulate.

assumptions (4)
  • standard math Classical higher-order logic as implemented in Isabelle/HOL, including excluded middle, choice, and infinity
    The entire development is mechanized in Isabelle/HOL, so all theorems depend on this logical foundation.
  • domain assumption Traces are finite or infinite sequences over states Sigma = P(A), with prefix, extension, and suffix operations as defined in Section 2
    This is the intended model class for LTL and LTL3; the isomorphism in Theorem 2 is stated over Sigma^infinity and Sigma^omega.
  • domain assumption The conventional LTL semantics in Figure 2 is the reference semantics
    Theorem 7 proves equivalence to this standard definition; it is a benchmark, not something the paper derives.
  • ad hoc to paper A 'sufficiently powerful simplifier' can decide semantic triviality, meaning whether the progressed formula's definitive set is the set of all traces
    Section 5, after Figure 5: soundness and completeness of formula progression are proven modulo this oracle, and the paper states that a syntactic simplifier characterization is outside its scope.
invented entities (1)
  • Definitive prefix sets (written with the black diamond operator) and answer-indexed families from truth values to definitive sets independent evidence
    purpose: Give LTL3 a compositional inductive semantics and represent good and bad prefixes structurally
    These are new mathematical definitions, but they are fully specified and supported by machine-checked theorems in Isabelle/HOL, so they are not unexplained postulates.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Semantics for Linear-time Temporal Logic with Finite Observations." pith.science (2026). https://pith.science/paper/CUDBMZKC

@misc{pith2026241114581,
  author       = {Pith},
  title        = {Pith review of: Semantics for Linear-time Temporal Logic with Finite Observations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CUDBMZKC}},
  note         = {Machine review of arXiv:2411.14581}
}
read the original abstract

LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by contrast, gives a full model-based inductive accounting of the semantics of LTL3, in terms of families of definitive prefix sets. We show that our definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby show that our semantics of LTL3 directly correspond to the semantics of conventional LTL. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics. All of our definitions and proofs are mechanised in Isabelle/HOL.

Figures

Figures reproduced from arXiv: 2411.14581 by the authors.

Figure 1
Figure 1. Syntax of LTL or the Brzozowski derivative. Bauer and Falcone [BF12] claim without proof that formula progression yields an equivalent semantics to LTL3. In this paper, we make this statement formally precise, and prove soundness and completeness (modulo a sufficiently powerful simplifier) of the formula progression technique with respect to our semantics. Finally in Section 6, we relate our work to other characteri… view at source ↗
Figure 2
Figure 2. Semantics of conventional LTL Bauer et al. [BLS11] describe LTL3 as a three-valued logic that interprets LTL formulae on finite prefixes to obtain a truth value in B3 = {T,F,?}. For a formula ϕ and a finite prefix t, the truth value T indicates that ϕ can be definitively established from t alone, whereas F indicates that ϕ can be definitively refuted from t alone. The third value ? indicates that the formula ϕ can n… view at source ↗
Figure 3
Figure 3. LTL semantics using answer-indexed families [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: LTL3 semantics using answer-indexed families For the U operator, we construct our semantics iteratively, building up by repeatedly prepending states. Here the notation f k indicates the self-composition of f k times, i.e. f 0 (x) = x and f k+1 (x) = f k ( f (x)): (Φ U …
Figure 5
Figure 5. Figure 5: Rules for formula progression ϕ = ϕ ′ ∧ψ ′ : Follows from inductive hypotheses as Pr preserves greatest lower and least upper bounds. ϕ = ϕ ′ : Follows from inductive hypotheses as the prepend operator ▷ commutes with Pr. ϕ = ϕ ′ U ψ ′ : Because Pr commutes with ▷ and …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 11 canonical work pages

  1. [1]

    , " * write output.state after.block = add.period write newline

    ENTRY address author booktitle chapter doi edition editor eid eprint howpublished institution journal key note number organization pages publisher school series title type url ee volume year label extra.label sort.label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence :=...

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  3. [3]

    , " * write output.state after.block = add.period write newline

    ENTRY address author booktitle chapter doi edition editor eid eprint howpublished institution journal key note number organization pages publisher school series title type url ee volume year label extra.label sort.label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence :=...

  4. [4]

    , " * write output.state after.block = add.period write newline

    ENTRY address author booktitle chapter doi edition editor eid eprint howpublished institution journal key note number organization pages publisher school series title type url ee volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := ...

  5. [5]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  6. [6]

    journal Proceedings of the ACM on Programming Languages volume 3 ( number POPL ), pp

    author Luca Aceto , author Antonis Achilleos , author Adrian Francalanza , author Anna Ing \'o lfsd \'o ttir & author Karoliina Lehtinen ( year 2019 ): title Adventures in monitorability: from branching to linear time and back again . journal Proceedings of the ACM on Programming Languages volume 3 ( number POPL ), pp. pages 1--29 , doi:10.1145/3290365. a...

    doi:10.1145/3290365 2019

  7. [7]

    journal Archive of Formal Proofs

    author Rayhana Amjad , author Rob van Glabbeek & author Liam O'Connor ( year 2024 ): title Definitive Set Semantics for LTL3 . journal Archive of Formal Proofs . note https://isa-afp.org/entries/LTL3_Semantics.html, Formal proof development . article alpernschneider

    work page 2024

  8. [8]

    Schneider ( year 1985 ): title Defining liveness

    author Bowen Alpern & author Fred B. Schneider ( year 1985 ): title Defining liveness . journal Information Processing Letters volume 21 ( number 4 ), pp. pages 181--185 , doi:10.1016/0020-0190(85)90056-0. inproceedings fpltl3fm

    doi:10.1016/0020-0190(85)90056-0 1985

Show all 27 references
  1. [9]

    In: booktitle FM 2012: Formal Methods , publisher Springer , pp

    author Andreas Bauer & author Yli \`e s Falcone ( year 2012 ): title Decentralised LTL Monitoring . In: booktitle FM 2012: Formal Methods , publisher Springer , pp. pages 85--100 , doi:10.1007/978-3-642-32759-9_10. inbook progress1

    2012 doi

  2. [10]

    pages 141–153

    author Fahiem Bacchus & author Froduald Kabanza ( year 1996 ): title Using Temporal Logic to Control Search in a Forward Chaining Planner , p. pages 141–153 . publisher IOS Press . inproceedings partiallogic

    1996

  3. [11]

    In: booktitle Handbook of Philosophical Logic , publisher Springer , pp

    author Stephen Blamey ( year 2002 ): title Partial Logic . In: booktitle Handbook of Philosophical Logic , publisher Springer , pp. pages 261--353 , doi:10.1007/978-94-017-0458-8\_5. inproceedings bauergbu

    2002 doi

  4. [12]

    pages 126--138 , doi:10.1007/978-3-540-77395-5_11

    author Andreas Bauer , author Martin Leucker & author Christian Schallhart ( year 2007 ): title The Good, the Bad, and the Ugly, But How Ugly Is Ugly? In: booktitle Runtime Verification , publisher Springer , pp. pages 126--138 , doi:10.1007/978-3-540-77395-5_11. article bauer...

    2007 doi

  5. [13]

    journal Journal of Logic and Computation volume 20 ( number 3 ), pp

    author Andreas Bauer , author Martin Leucker & author Christian Schallhart ( year 2010 ): title Comparing LTL Semantics for Runtime Verification . journal Journal of Logic and Computation volume 20 ( number 3 ), pp. pages 651--674 , doi:10.1093/logcom/exn075. article ltl3tosem

    2010 doi

  6. [14]

    journal ACM Transactions on Software Engineering Methodology volume 20 ( number 4 ), doi:10.1145/2000799.2000800

    author Andreas Bauer , author Martin Leucker & author Christian Schallhart ( year 2011 ): title Runtime Verification for LTL and TLTL . journal ACM Transactions on Software Engineering Methodology volume 20 ( number 4 ), doi:10.1145/2000799.2000800. inproceedings safetyprogress

    2011

  7. [15]

    In: booktitle Logic and Algebra of Specification , publisher Springer , pp

    author Edward Chang , author Zohar Manna & author Amir Pnueli ( year 1993 ): title The Safety-Progress Classification . In: booktitle Logic and Algebra of Specification , publisher Springer , pp. pages 143--202 , doi:10.1007/978-3-642-58041-3_5. inproceedings chai

    1993 doi

  8. [16]

    In: booktitle IEEE 44th International Symposium on Multiple-Valued Logic , pp

    author Ming Chai & author Bernd-Holger Schlingloff ( year 2014 ): title Online Monitoring of Distributed Systems with a Five-Valued LTL . In: booktitle IEEE 44th International Symposium on Multiple-Valued Logic , pp. pages 226--231 , doi:10.1109/ISMVL.2014.47. inproceedings ltlpm

    2014 doi

  9. [17]

    In: booktitle Computer Aided Verification , publisher Springer , pp

    author Cindy Eisner , author Dana Fisman , author John Havlicek , author Yoad Lustig , author Anthony McIsaac & author David Van Campenhout ( year 2003 ): title Reasoning with Temporal Logic on Truncated Paths . In: booktitle Computer Aided Verification , publisher Springer , ...

    2003 doi

  10. [18]

    Henzinger , author Nicolas Mazzocchi & author N

    author Thomas A. Henzinger , author Nicolas Mazzocchi & author N. Ege Sara c ( year 2023 ): title Quantitative Safety and Liveness . In: booktitle Foundations of Software Science and Computation Structures , publisher Springer , pp. pages 349--370 , doi:10.1007/978-3-031-30829...

    2023 doi

  11. [19]

    In: booktitle International Conference on Automated Planning and Scheduling , publisher AAAI , pp

    author Froduald Kabanza & author Sylvie Thi \' e baux ( year 2005 ): title Search Control in Planning for Temporally Extended Goals . In: booktitle International Conference on Automated Planning and Scheduling , publisher AAAI , pp. pages 130--139 . article kupfermanvardi

    2005

  12. [20]

    Vardi ( year 2001 ): title Model Checking of Safety Properties

    author Orna Kupferman & author Moshe Y. Vardi ( year 2001 ): title Model Checking of Safety Properties . journal Formal Methods in System Design volume 19 ( number 3 ), pp. pages 291--314 , doi:10.1023/A:1011254632723. article Lam77

    2001 doi

  13. [21]

    journal IEEE Transactions on Software Engineering volume 3 ( number 2 ), pp

    author Leslie Lamport ( year 1977 ): title Proving the correctness of multiprocess programs . journal IEEE Transactions on Software Engineering volume 3 ( number 2 ), pp. pages 125--143 , doi:10.1109/TSE.1977.229904. inproceedings fltl

    1977

  14. [22]

    In: booktitle Logics of Programs , publisher Springer , pp

    author Orna Lichtenstein , author Amir Pnueli & author Lenore Zuck ( year 1985 ): title The Glory of the Past . In: booktitle Logics of Programs , publisher Springer , pp. pages 196--218 , doi:10.1007/3-540-15648-8_16. book ltl

    1985 doi

  15. [23]

    publisher Springer , doi:10.1007/978-1-4612-0931-7

    author Zohar Manna & author Amir Pnueli ( year 1992 ): title The Temporal Logic of Reactive and Concurrent Systems . publisher Springer , doi:10.1007/978-1-4612-0931-7. book ltlsafety

    1992 doi

  16. [24]

    publisher Springer , doi:10.1007/978-1-4612-4222-2

    author Zohar Manna & author Amir Pnueli ( year 1995 ): title Temporal Verification of Reactive Systems: Safety . publisher Springer , doi:10.1007/978-1-4612-4222-2. inproceedings quickstrom

    1995 doi

  17. [25]

    In: booktitle Programming Language Design and Implementation , series PLDI 2022 , publisher ACM , p

    author Liam O'Connor & author Oskar Wickstr\" o m ( year 2022 ): title Quickstrom: Property-based Acceptance Testing with LTL Specifications . In: booktitle Programming Language Design and Implementation , series PLDI 2022 , publisher ACM , p. pages 1025–1038 , doi:10.1145/351...

    2022

  18. [26]

    journal Automated Software Engineering volume 12 ( number 2 ), pp

    author Grigore Ro s u & author Klaus Havelund ( year 2005 ): title Rewriting-Based Techniques for Runtime Verification . journal Automated Software Engineering volume 12 ( number 2 ), pp. pages 151--197 , doi:10.1007/s10515-005-6205-y. inproceedings rltl

    2005 doi

  19. [27]

    author Paulo Tabuada & author Daniel Neider ( year 2016 ): title Robust Linear Temporal Logic . In: booktitle 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 , series Leibniz International Proceedings in Informatics (LIPIcs) volume 62 , publisher Schloss Dagst...

    2016 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.