LTL to Smaller Self-Loop Alternating Automata and Back

Franti\v{s}ek Blahoudek; Jan Strej\v{c}ek; Juraj Major

REVIEW 3 major objections 4 minor 27 references

LTL to Smaller Self-Loop Alternating Automata and Back

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read Every LTL formula translates into a self-loop alternating automaton with mixed Fin/Inf acceptance, and the translation back to LTL is exact.

desk verdict Genuinely new LTL-to-SLAA translation work with real practical gains, but the main correctness proof has a load-bearing unproved lemma (Proposition 1) that a serious referee must ask to be fixed. read the letter →

arxiv 1908.04645 v2 pith:QZLSL7PX submitted 2019-08-13 cs.FL

František Blahoudek , Juraj Major , Jan Strejček This is my paper · ORCID

classification cs.FL MSC 03B4468Q4568Q60

keywords lineartemporallogicself-loopalternatingautomataEmerson-Leiacceptanceinfinitewordstranslationverificationconditionsstatemerging

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

Self-loop alternating automata (SLAA) are standard intermediates in translating linear temporal logic into automata that verification tools can use; previously they always used Büchi or co-Büchi acceptance. This paper shows that switching to a generic Emerson-Lei acceptance condition — a positive boolean combination of "this mark appears finitely often" and "this mark appears infinitely often" — makes the intermediate automata considerably smaller at no cost in language. Theorem 1 proves that the F,G-merging translation produces an equivalent SLAA with linearly many states, and Theorem 2 proves the reverse translation from any SLAA back to LTL is exact. The practical payoff is that F- and G-rich formulas, common in verification, produce automata with up to 45% fewer states, and many more of them are deterministic or purely existential.

What carries the argument

The load-bearing object is the F,G-merging construction itself: for subformulas $F\psi$, it expands $\psi$ into disjunctive normal form over temporal formulas and merges the state $F\psi$ with the resulting states $\psi_K$; for subformulas $G\bigwedge_i \psi_i$, it merges $G\psi$ with its conjunct states. The move that makes correctness work is the use of acceptance marks to track escaping multitransitions: a transition that leaves a merged state is marked, and the acceptance formula such as $\mathrm{Fin}_\psi \lor \mathrm{Inf}_\psi$ for each $U$-subformula accepts a branch exactly when it would have been accepted under the unmerged translation. The proof relies on Proposition 1, which lets accepting runs over suffixes of one word be synchronized into a single run, and on the observation that a mark with a single owner is satisfied finitely-often exactly when either the mark appears finitely often or the owner state is escaped infinitely often.

What would settle it

Enumerate all LTL formulas up to some fixed size, build the F,G-merging automaton for each, and test language equivalence against a reference translator: any mismatch falsifies Theorem 1. A more surgical test is to search for a word with two suffixes each accepted by some SLAA but with no pair of accepting runs whose transitions can be synchronized, which would refute Proposition 1 and the induction that carries the proof.

Watch

Extended reading notes

Core claim

The paper's central claim is that the self-loop restriction of alternating automata does not force Büchi or co-Büchi acceptance. Its F,G-merging translation builds, for every LTL formula $\varphi$, an SLAA $A_\varphi$ whose language is exactly $L(\varphi)$; the automaton has one state per subformula, so $O(|\varphi|)$ states, and an acceptance condition that may use both Fin and Inf marks, with at most exponentially many marks. The translation merges the state for $F\psi$ with states for the temporal disjuncts of $\psi$, and merges $G\psi$ with the states for its conjuncts, adjusting the acceptance formula with marks that record escaping multitransitions. The same expressive power is established by an explicit translation of any SLAA back to an equivalent LTL formula. The empirical claim, supported by measurements on literature and randomly generated formulas, is that these merged automata are often much smaller — over 45% fewer states in the F/G-heavy benchmark — and are more often deterministic or nonalternating.

Load-bearing premise

Everything in the correctness proof rests on Proposition 1, stated without proof in the appendix: any two accepting runs of an SLAA over suffixes of the same word can be chosen so their transitions line up into a single valid run, and if that fails the language-equality argument collapses.

Editorial extensions

If this is right

Every LTL formula now has an equivalent SLAA with transition-based Emerson-Lei acceptance, and conversely every such SLAA has an equivalent LTL formula; the two formalisms have the same expressive power.
The F,G-merging forward translation keeps the state count linear in formula size and bounds the number of acceptance marks exponentially, so it is asymptotically no worse than traditional Büchi or co-Büchi translations while offering better constants.
On formulas dominated by F and G operators, the construction saves over 45% of states on random benchmarks and turns many alternating automata into deterministic or purely existential ones.
Because the back-translation is exact, SLAA can be used as a lossless intermediate in pipelines that translate LTL to deterministic or nondeterministic automata.
The transition-dominance simplification extends to arbitrary Emerson-Lei acceptance, so smaller automata do not have to sacrifice post-construction simplification.

Reading between the lines

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

The merging trick is asymmetric: it uses DNF for F and CNF for G, so a dual construction that merges $G\psi$ with disjunctive components, or $F\psi$ with conjunctive normal forms, might close the remaining gap and shrink automata for formulas the current rules cannot touch.
The single-owner observation behind the escaping-mark argument is general; any temporal operator whose semantics can be expressed by "eventually, and then always" style conditions may be mergeable by the same discipline of re-marking escaping transitions.
Because realistic verification specifications are rich in F and G patterns, the 45% savings on random F/G-heavy formulas likely understates the practical benefit on engineered specifications; this is a testable prediction against industrial pattern benchmarks.
Composing the forward and backward translations gives an LTL-to-LTL normalization that, combined with the smaller automata, may be useful for formula simplification outside automaton construction.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Two things to know. First, this is the first LTL-to-SLAA translation targeting transition-based Emerson-Lei acceptance, and the F-merging and F,G-merging constructions do produce smaller SLAA on F/G-heavy formulas — about 45% state savings on their randfg benchmark, with more deterministic and nonalternating outputs. Second, the correctness proof of the main theorem has a load-bearing hole: Proposition 1, which guarantees mutually synchronized accepting runs for suffixes and across different automata, is stated without proof. I could not find a counterexample, and the proposition may well be true, but as written it is not a routine detail. The stress-test note is right to flag that the G-case applies it to infinitely many runs at once, which is exactly where conflicts in multitransition unions would hide if they exist.

What is actually new: the F-merging and F,G-merging transformations (including the Inf-less intermediate class), the SLAA-to-LTL back-translation for Emerson-Lei acceptance, and the generalized transition-dominance simplification. The experiments are honest, with published scripts and a notebook; the fact that the basic translation reproduces LTL3BA's numbers gives some confidence the implementation is not drifting. The citation pattern is appropriate, and the self-citations are grounded in released tools.

The soft spots, in proportion. Proposition 1 is the main one; the paper's central Theorem 1 leans on it, and the appendix only asserts it. Theorem 2's 'straightforward by induction' is a sketch, but that back-translation looks more standard and the risk is lower. The DNF decomposition for F-subformulae can blow up the number of acceptance marks; they acknowledge this and state the exponential bound, so it is a cost, not a hidden flaw. The experimental comparison is on random formulas plus a small literature set, and the headline 45% saving comes from a benchmark biased toward F and G, so I would not generalize too far.

Who this is for: anyone building LTL-to-automata pipelines or studying alternating automata with Emerson-Lei acceptance. It deserves a serious referee rather than a desk rejection. The right outcome is major revision: turn Proposition 1 into a real lemma with a proof (or weaken it to what the composition arguments actually need), and expand the proof of Theorem 2. I would not reject it on the current evidence.

Referee Report

3 major / 4 minor

Summary. The paper considers self-loop alternating automata (SLAA) with transition-based Emerson-Lei acceptance and presents two main results. First, it gives a sequence of translations from LTL to SLAA: a baseline co-Büchi construction, an F-merging variant producing Inf-less SLAA, and an F,G-merging variant producing SLAA with mixed Fin/Inf acceptance; Theorem 1 claims that the final translation is correct, has linearly many states, and at most exponentially many acceptance marks. Second, it gives a back-translation from SLAA with Emerson-Lei acceptance to LTL (Theorem 2), establishing equal expressive power. The paper also defines transition dominance for EL acceptance and reports experiments with the LTL3TELA tool showing state reductions on mergeable formulae.

Significance. The contribution is potentially valuable: the F,G-merging construction is a parameter-free, implemented translation that exploits generic acceptance for smaller intermediate automata, and the experiments indicate substantial savings on F/G-heavy formula sets, including more deterministic and nonalternating automata. The authors also provide a Jupyter notebook with the benchmark data, which is a concrete reproducibility strength. However, the central correctness proofs are not yet watertight: the synchronization lemma (Proposition 1) is used as a black box and the back-translation proof is only sketched. The expressiveness equivalence and the empirical claims depend on these results, so the paper needs a revision that supplies the missing arguments.

major comments (3)

[Appendix A, Proposition 1] Proposition 1 is stated without proof and is load-bearing: it is invoked to compose accepting runs of subformula automata in every case of the inclusion L(φ) ⊆ L(Aφ), and in the G-case it is applied to infinitely many runs simultaneously. As written, the proof gives no argument that two accepting runs over suffixes of the same word can always be chosen so that their unions at each position are valid multitransitions, nor that this extends to runs of different automata. If this lemma fails, the constructed T_i are not guaranteed to be multitransitions and the proof of Theorem 1 collapses. Please provide a full proof of Proposition 1, or replace it with an explicit coinductive composition argument.
[Section 7, Theorem 2] The proof of Theorem 2 is a single sentence saying the statement follows by induction. The construction of φ(s) uses nested U and G operators whose semantics depend on infinite behavior, and the induction over the partial order must verify that runs that leave s after finitely many self-loops satisfy φ1(s) while runs that never leave s satisfy φ2(s) ∧ φ3(s). This is not a routine detail for a result establishing expressiveness equivalence; please include the induction in the appendix.
[Appendix A, G-case of L(Aφ) ⊆ L(φ)] In the G-case of the reverse inclusion, the runs σψ_i are defined by the equation σψ_i = {t}(Ti+1[C′_i]... ⊔ σψ_{i+1}), which is an infinite regress rather than a well-founded induction. The proof needs to justify that the ⊔ operation produces valid multitransitions and that the resulting infinite runs are accepting; otherwise the claim that each σψ_i is accepting is unsupported.

minor comments (4)

[Section 5] The two different mark symbols for each U and F subformula (e.g., ψ and ψ, or Fψ and Fψ) are not visually distinguished in the text. Since the correctness of the acceptance clauses depends on which mark is placed on the U-loop and the F-tt-loop, please clarify the notation.
[Appendix A, Fψ case] The sentence 'no ϕ appears in the run, so both Fin_ϕ and Fin_K_ϕ for some K ∈ ψ holds' is imprecise: the acceptance clause for Fψ is a disjunction with Inf_{Fψ}, and the proof should explicitly exclude the Inf case.
[Section 8.3] The sentence 'Furter, the F-merging...' contains a typo ('Furter' should be 'Further').
[References] References [4] and [17] are marked 'To appear'; if the publication details are now available, please update them.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the F,G-merging translation is defined independently and its correctness is proved by structural induction against the LTL semantics, while the claimed state reductions are measured experimentally.

full rationale

The paper's central load-bearing results are Theorem 1 (L(A_phi) = L(phi) for the F,G-merging translation) and Theorem 2 (SLAA back to LTL). Neither theorem uses a fitted parameter or a quantity defined in terms of the target result. The transition rules in Sections 3, 4, and 5 are explicit constructions, and Appendix A proves correctness by structural induction on the LTL formula, composing accepting runs of subformula automata; acceptance marks are introduced to encode U/F/G semantics and checked against the external satisfaction relation. The experimental section measures state counts and acceptance marks on fixed LTL3BA/basic-translation baselines; no parameter is fitted to those benchmarks and then renamed a prediction. The paper cites prior work by the same authors (e.g., the HOA format, LTL3BA, ltl3tela) but only as context or baseline, not as the justification for the claimed equivalence. One genuine caveat is flagged: Appendix A's Proposition 1, asserting that accepting runs over suffixes can always be chosen synchronized, is stated without proof and is used in the composability steps, especially the G-case. This is a completeness and rigor weakness, not circularity: the proposition is an auxiliary mathematical lemma, and no equation in the paper defines L(A_phi) or the acceptance formula in terms of the theorem's conclusion. The back-translation (Theorem 2) is also sketched rather than detailed, but again this is an omitted proof detail, not a reduction of the claim to its own input. Therefore no circular step is exhibited and the score is 0.

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

No numerical parameters are fitted and no new semantic entities are introduced. The only nonstandard unproved ingredient is the synchronization proposition, which is an assumption about runs of the already-defined automaton model.

assumptions (4)

standard math Standard semantics of LTL in positive normal form, as defined in Section 2.1.
The translations are proven against this semantics; it is the standard definition of the logic.
domain assumption Definition of SLAA with transition-based Emerson-Lei acceptance in Section 2.2, including the run and branch acceptance semantics.
The paper's results are about this specific automaton model and acceptance definition.
ad hoc to paper Proposition 1: accepting runs over suffixes of the same word can always be chosen synchronized.
Used throughout the correctness proof in Appendix A for the U, F, and G cases, but not proved.
domain assumption The alphabet of an automaton has the form 2^AP' for a finite set of atomic propositions.
Used in the back-translation to define the formulas phi_alpha over propositional literals.

how reviews work

0 comments

Cite this review

Pith. "Pith review of LTL to Smaller Self-Loop Alternating Automata and Back." pith.science (2026). https://pith.science/paper/QZLSL7PX

@misc{pith2026190804645,
  author       = {Pith},
  title        = {Pith review of: LTL to Smaller Self-Loop Alternating Automata and Back},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QZLSL7PX}},
  note         = {Machine review of arXiv:1908.04645}
}

read the original abstract

Self-loop alternating automata (SLAA) with B\"uchi or co-B\"uchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to B\"uchi or co-B\"uchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.

Figures

Figures reproduced from arXiv: 1908.04645 by the authors.

**Figure 1.** Automata for the formula ϕ = F(Ga ∨ GFb): the co-B¨uchi SLAA produced by the basic translation (left), the Inf-less SLAA produced by F-merging (middle), and the SLAA produced by F,G-merging (right). Graphical notation is explained in Section 2. This paper presents a translation of LTL to SLAA with transition-based Emerson-Lei acceptance. The translation aims to take advantage of the generic acceptance and produce SL… view at source ↗

**Figure 2.** Automata for Fψ: the SLAA A built by the basic translation (left) and the SLAA AF built by the F-merging translation (right). state. However, we can modify the translation rules to make ψ reachable and a R b unreachable at the same time. The modification is based on the following observation. Taking the red bc-edge in A would mean that both a R b and Gc have to hold in the next step, which is equivalent to (a R b) ∧… view at source ↗

**Figure 3.** Automata for F((aR b) ∧ Gc): the SLAA A built by the basic translation (left) and the modified SLAA A ′ where states in the grey area can be merged (right) [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

Figures from the paper (3 more)

**Figure 4.** Figure 4: Transitions of the state F(ψ1 ∨ ψ2 ∨ ψ3) merged with states ψ1, ψ2, and ψ3. of the merged automaton that contain infinitely many loops corresponding to two or more different states ψi should be nonaccepting. Therefore we adjust the acceptance formula to Fin ∧(Fin 1 ∨Fi…

**Figure 5.** Figure 5: An SLAA A for the formula GFa built by the basic translation (top) and an equivalent SLAA AF,G built by the F,G-merging translation (bottom) and their runs over the word (∅∅{a}) ω . the states into one that corresponds to their conjunction (Gψ) ∧ ψ, which is equivalent…

**Figure 6.** Figure 6: Effect of F,G-merging on SLAA size for mergeable formulae. A dot represents the number of states of the SLAA produced by F,G-merging (y-axis) and by the basic translation (x-axis) for the same formula. The color of the dot reflects the number of dots at the position. f…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

[1]

The Hanoi Omega-Automata Forma t

T. Babiak, F. Blahoudek, A. Duret-Lutz, J. Klein, J. Kˇ ret ´ ınsk´ y, D. M¨ uller, D. Parker, and J. Strejˇ cek.“The Hanoi Omega-Automata Forma t”. In: Proc. of CAV’15. LNCS 9206.I, pp. 479–486. Springer, 2015

work page 2015
[2]

Eﬀective Trans- lation of LTL to Deterministic Rabin Automata: Beyond the (F, G)- Fragment

T. Babiak, F. Blahoudek, M. Kˇ ret ´ ınsk´ y, and J. Strejˇ cek.“Eﬀective Trans- lation of LTL to Deterministic Rabin Automata: Beyond the (F, G)- Fragment”. In: Proc. of ATVA’13. LNCS 8172, pp. 24–39. Springer, 2013

work page 2013
[3]

LTL to B¨ uchi Au- tomata Translation: Fast and More Deterministic

T. Babiak, M. Kˇ ret ´ ınsk´ y, V.ˇReh´ ak, and J. Strejˇ cek.“LTL to B¨ uchi Au- tomata Translation: Fast and More Deterministic”. In: Proc. of TACAS’12. LNCS 7214, pp. 95–109. Springer, 2012

work page 2012
[4]

Generic Emptiness Check for Fun and Proﬁt

C. Baier, F. Blahoudek, A. Duret-Lutz, J. Klein, D. M¨ uller, and J . Strejˇ cek.“Generic Emptiness Check for Fun and Proﬁt”. In: Proc. of ATVA’19. LNCS. To appear. Springer

work page
[5]

Automata withGeneralized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis

K. Chatterjee, A. Gaiser, and J. Kˇ ret ´ ınsk´ y.“Automata withGeneralized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis”. In: Proc. of CAV’13. LNCS 8044, pp. 559–575. Springer, 2013

work page 2013
[6]

On-the-F ly Emptiness Checks for Generalized B¨ uchi Automata

J.-M. Couvreur, A. Duret-Lutz, and D. Poitrenaud.“On-the-F ly Emptiness Checks for Generalized B¨ uchi Automata”. In: Proc. of SPIN’05 . LNCS 3639, pp. 169–184. Springer, 2005

work page 2005
[7]

Manipulating LTL Formulas Using Spot 1.0

A. Duret-Lutz.“Manipulating LTL Formulas Using Spot 1.0”. In: Proc. of ATVA’13. LNCS 8172, pp. 442–445. Springer, 2013

work page 2013
[8]

Spot 2.0 - A Framework for LTL and ω -Automata Manipulation

A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renau lt, and L. Xu.“Spot 2.0 - A Framework for LTL and ω -Automata Manipulation”. In: Proc. of ATVA’16. LNCS 9938, pp. 122–129. 2016

work page 2016

Show all 27 references

[9]

Property Speciﬁ cation Patterns for Finite-State Veriﬁcation

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett.“Property Speciﬁ cation Patterns for Finite-State Veriﬁcation”. In: Proc. of FMSP’98 , pp. 7–15. ACM, 1998

1998
[10]

Modalities for Model Checking: Bra nch- ing Time Logic Strikes Back

E. A. Emerson and C.-L. Lei. “Modalities for Model Checking: Bra nch- ing Time Logic Strikes Back”. In: Science of Computer Programming 8.3 (1987), pp. 275–306

1987
[11]

Optimizing B¨ uchi Automata

K. Etessami and G. J. Holzmann.“Optimizing B¨ uchi Automata”. In: Proc. of CONCUR’00. LNCS 1877, pp. 153–167. Springer, 2000

2000
[12]

Fast LTL to B¨ uchi Automata Transla tion

P. Gastin and D. Oddoux.“Fast LTL to B¨ uchi Automata Transla tion”. In: Proc. of CAV’01. LNCS 2102, pp. 53–65. Springer, 2001

2001
[13]

Truly On-the-Fly LTL Model Check- ing

M. Hammer, A. Knapp, and S. Merz.“Truly On-the-Fly LTL Model Check- ing”. In: Proc. of TACAS’05. LNCS 3440, pp. 191–205. Springer, 2005

2005
[14]

Holeˇ cek, T

J. Holeˇ cek, T. Kratochv ´ ıla, V.ˇReh´ ak, D.ˇSafr´ anek, and P.ˇSimeˇ cek.Veri- ﬁcation Results in Liberouter Project . Tech. rep. 03, 32pp. CESNET, Sept. 2004

2004
[15]

Rabinizer 4: From LTL to Your Favourite Deterministic Automaton

J. Kˇ ret ´ ınsk´ y, T. Meggendorfer, S. Sickert, and C. Ziegler .“Rabinizer 4: From LTL to Your Favourite Deterministic Automaton”. In: Proc. of CAV’18. LNCS 10981, pp. 567–577. Springer, 2018

2018
[16]

Alternating Automata and Logics ove r Inﬁnite Words

C. L¨ oding and W. Thomas.“Alternating Automata and Logics ove r Inﬁnite Words”. In: Proc. of IFIP TCS’00 . LNCS 1872, pp. 521–535. Springer, 2000. 20 REFERENCES

2000
[17]

ltl3tela: LTL to Small Deterministic or Nondeterminis- tic Emerson-Lei Automata

J. Major, F. Blahoudek, J. Strejˇ cek, M. Sasar´ akov´ a, an d T. Zbonˇ c´ akov´ a.“ltl3tela: LTL to Small Deterministic or Nondeterminis- tic Emerson-Lei Automata”. In: Proc. of ATVA’19 . LNCS. To appear. Springer
[18]

Weak Alternating Auto mata Give a Simple Explanation of Why Most Temporal and Dynamic Logics are Decidable in Exponential Time

D. E. Muller, A. Saoudi, and P. E. Schupp.“Weak Alternating Auto mata Give a Simple Explanation of Why Most Temporal and Dynamic Logics are Decidable in Exponential Time”. In: Proc. of LICS ’88 , pp. 422–427. IEEE Computer Society, 1988

1988
[19]

LTL to Deterministic Emerson-Lei Aut omata

D. M¨ uller and S. Sickert.“LTL to Deterministic Emerson-Lei Aut omata”. In: Proc. of GandALF’17. EPTCS 256, pp. 180–194. 2017

2017
[20]

BEEM: Benchmarks for Explicit Model Checkers

R. Pel´ anek.“BEEM: Benchmarks for Explicit Model Checkers”. In: Proc. of SPIN’07. LNCS 4595, pp. 263–267. Springer, 2007

2007
[21]

Deeper Connections Between L TL and Al- ternating Automata

R. Pel´ anek and J. Strejˇ cek.“Deeper Connections Between L TL and Al- ternating Automata”. In: Proc. of CIAA’05 . LNCS 3845, pp. 238–249. Springer, 2005

2005
[22]

The Temporal Logic of Programs

A. Pnueli.“The Temporal Logic of Programs”. In: Proc. of FOCS’77 , pp. 46–57. IEEE Computer Society, 1977

1977
[23]

Pa rallel Ex- plicit Model Checking for Generalized B¨ uchi Automata

E. Renault, A. Duret-Lutz, F. Kordon, and D. Poitrenaud.“Pa rallel Ex- plicit Model Checking for Generalized B¨ uchi Automata”. In: Proc. of TACAS’15. LNCS 9035, pp. 613–627. Springer, 2015

2015
[24]

Alternating Automata and the Temporal Logic of Ordinals

G. S. Rohde. “Alternating Automata and the Temporal Logic of Ordinals”. PhD thesis. University of Illinois at Urbana-Champaign, 1997. isbn: 0-591- 63604-2

1997
[25]

Eﬃcient B¨ uchi Automata from LTL Fo rmulae

F. Somenzi and R. Bloem.“Eﬃcient B¨ uchi Automata from LTL Fo rmulae”. In: Proc. of CAV’00. LNCS 1855, pp. 248–263. Springer, 2000

2000
[26]

Automata and Linear Temporal Logic: Translat ions with Transition-Based Acceptance

H. Tauriainen. “Automata and Linear Temporal Logic: Translat ions with Transition-Based Acceptance”. PhD thesis. Helsinki University of Tech- nology, Laboratory for Theoretical Computer Science, 2006. isbn: 951-22- 8343-3

2006
[27]

Nontraditional Applications of Automata Theory

M. Y. Vardi.“Nontraditional Applications of Automata Theory”. In: Proc. of TACS’94. LNCS 789, pp. 575–597. Springer, 1994. REFERENCES 21 A Correctness and Complexity of the F, G-Merging Translation Theorem 1. Let ϕ be an LTL formula and let Aϕ be the corresponding SLAA built b...

1994

Pith tools

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

[1] [1]

The Hanoi Omega-Automata Forma t

T. Babiak, F. Blahoudek, A. Duret-Lutz, J. Klein, J. Kˇ ret ´ ınsk´ y, D. M¨ uller, D. Parker, and J. Strejˇ cek.“The Hanoi Omega-Automata Forma t”. In: Proc. of CAV’15. LNCS 9206.I, pp. 479–486. Springer, 2015

work page 2015

[2] [2]

Eﬀective Trans- lation of LTL to Deterministic Rabin Automata: Beyond the (F, G)- Fragment

T. Babiak, F. Blahoudek, M. Kˇ ret ´ ınsk´ y, and J. Strejˇ cek.“Eﬀective Trans- lation of LTL to Deterministic Rabin Automata: Beyond the (F, G)- Fragment”. In: Proc. of ATVA’13. LNCS 8172, pp. 24–39. Springer, 2013

work page 2013

[3] [3]

LTL to B¨ uchi Au- tomata Translation: Fast and More Deterministic

T. Babiak, M. Kˇ ret ´ ınsk´ y, V.ˇReh´ ak, and J. Strejˇ cek.“LTL to B¨ uchi Au- tomata Translation: Fast and More Deterministic”. In: Proc. of TACAS’12. LNCS 7214, pp. 95–109. Springer, 2012

work page 2012

[4] [4]

Generic Emptiness Check for Fun and Proﬁt

C. Baier, F. Blahoudek, A. Duret-Lutz, J. Klein, D. M¨ uller, and J . Strejˇ cek.“Generic Emptiness Check for Fun and Proﬁt”. In: Proc. of ATVA’19. LNCS. To appear. Springer

work page

[5] [5]

Automata withGeneralized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis

K. Chatterjee, A. Gaiser, and J. Kˇ ret ´ ınsk´ y.“Automata withGeneralized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis”. In: Proc. of CAV’13. LNCS 8044, pp. 559–575. Springer, 2013

work page 2013

[6] [6]

On-the-F ly Emptiness Checks for Generalized B¨ uchi Automata

J.-M. Couvreur, A. Duret-Lutz, and D. Poitrenaud.“On-the-F ly Emptiness Checks for Generalized B¨ uchi Automata”. In: Proc. of SPIN’05 . LNCS 3639, pp. 169–184. Springer, 2005

work page 2005

[7] [7]

Manipulating LTL Formulas Using Spot 1.0

A. Duret-Lutz.“Manipulating LTL Formulas Using Spot 1.0”. In: Proc. of ATVA’13. LNCS 8172, pp. 442–445. Springer, 2013

work page 2013

[8] [8]

Spot 2.0 - A Framework for LTL and ω -Automata Manipulation

A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renau lt, and L. Xu.“Spot 2.0 - A Framework for LTL and ω -Automata Manipulation”. In: Proc. of ATVA’16. LNCS 9938, pp. 122–129. 2016

work page 2016