pith. sign in

arxiv: 1907.02887 · v1 · pith:7M2KBEZCnew · submitted 2019-07-05 · 💻 cs.FL

From LTL to Unambiguous B\"uchi Automata via Disambiguation of Alternating Automata

Simon Jantsch , David M\"uller , Christel Baier , Joachim Klein This is my paper

Pith reviewed 2026-05-25 01:36 UTC · model grok-4.3

classification 💻 cs.FL
keywords LTLunambiguous Büchi automatavery weak alternating automatadisambiguationautomata constructionmodel checkingMarkov chains
0
0 comments X

The pith

A disambiguation procedure on very weak alternating automata produces unambiguous Büchi automata from LTL formulas.

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

The paper develops an algorithm that first translates an LTL formula into a very weak alternating automaton and then disambiguates it to obtain an unambiguous Büchi automaton. A new definition of unambiguity for very weak alternating automata underpins the disambiguation step and avoids the direct tableau constructions used in prior methods. The construction incorporates VWAA-level optimizations together with targeted LTL simplifications that aim to keep the final automata small. Experiments implemented in the duggi tool compare the resulting automaton sizes and runtimes against the tableau-based LTL-to-UBA procedure in SPOT and also evaluate the automata on Markov-chain analysis tasks.

Core claim

The central claim is that an LTL formula can be converted to an unambiguous Büchi automaton by first building a very weak alternating automaton and then applying a disambiguation procedure that rests on a new unambiguity notion for VWAA; the procedure is claimed to preserve language equivalence while the added optimizations and simplifications reduce size.

What carries the argument

The disambiguation procedure for very weak alternating automata that converts them into equivalent unambiguous Büchi automata using the new unambiguity definition.

If this is right

  • The generated unambiguous Büchi automata can be used directly for the analysis of Markov chains under LTL specifications.
  • VWAA-level optimizations and LTL simplifications yield smaller automata than unoptimized tableau translations.
  • The method supplies an alternative construction path whose size and runtime characteristics differ from those of existing tableau-based LTL-to-UBA translations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The intermediate VWAA representation may simplify combination with other automata constructions that already operate on alternating automata.
  • The same disambiguation idea could be tested on fragments of LTL or on related temporal logics to see whether size gains carry over.
  • If the produced UBA remain competitive on larger benchmarks, the approach could be integrated into existing verification tool chains that already rely on unambiguous automata.

Load-bearing premise

The new unambiguity definition for very weak alternating automata is sufficient to guarantee that the disambiguation step produces an unambiguous Büchi automaton that is language-equivalent to the original LTL formula.

What would settle it

An LTL formula for which the output Büchi automaton either accepts a word outside the language of the formula or accepts some word via two distinct runs would falsify the correctness of the disambiguation.

Figures

Figures reproduced from arXiv: 1907.02887 by Christel Baier, David M\"uller, Joachim Klein, Simon Jantsch.

Figure 1
Figure 1. Figure 1: The LTL-to-UBA step. A sequence of unambiguity checks and disam [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Overview of the general LTL-to-UBA generation algorithm. The LTL [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Disambiguation scheme for a source state [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Three VWAA for ♦a. The automaton in (b) is the result of standard disambiguation and (c) is the result of the modified transformation applied to (a). The automaton in (c) is non-deterministic and has two looping states, whereas (b) is not non-deterministic and has three looping states. size estimate of GA in our construction is 4n. However, no state in trim(GA) can contain both s and s˜ for any state s of … view at source ↗
Figure 5
Figure 5. Figure 5: Non-WDBA-recognizable fragment of ltlstore (948 formulas). Every point stands for a formula where the according automaton size for Duggi is the abcissa, the automaton size of ltl2tgba the ordinate. Points above the line stand for formulas where Duggi performed better. and returns the one with fewer states. Our formula set contains 472 formulas that are WDBA-recognizable and for which we could compute the m… view at source ↗
Figure 6
Figure 6. Figure 6: UBA sizes for two sets of parametrized formulas. [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Time consumption for translating and model checking [PITH_FULL_IMAGE:figures/full_fig_p014_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Model checking times for the cluster protocol with [PITH_FULL_IMAGE:figures/full_fig_p014_8.png] view at source ↗
Figure 22
Figure 22. Figure 22: Model checking times for the cluster workstation protocol for the formula [PITH_FULL_IMAGE:figures/full_fig_p031_22.png] view at source ↗
read the original abstract

This paper proposes a new algorithm for the generation of unambiguous B\"uchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool duggi and discuss experimental results that compare the automata sizes and computation times of duggi with the tableau-based LTL-to-UBA translation of the SPOT tool set. Our experiments also cover the analysis of Markov chains under LTL specifications, which is an important application of UBA.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper proposes a new algorithm to translate LTL formulas into unambiguous Büchi automata (UBA) that routes through very weak alternating automata (VWAA) as an intermediate representation. It defines a new notion of unambiguity for VWAA, supplies a disambiguation procedure that converts such VWAA into UBA, introduces VWAA-level optimizations together with targeted LTL simplifications, and reports an implementation in the duggi tool whose output sizes and runtimes are compared experimentally against the tableau-based LTL-to-UBA construction inside SPOT; the experiments also include the use of the resulting UBA for Markov-chain analysis under LTL specifications.

Significance. If the central construction is correct, the work supplies a genuinely different route from the dominant tableau-based LTL-to-UBA translations and demonstrates, via implementation and experiments, that the route can be made practical. The explicit comparison on automata size and runtime, together with the Markov-chain application, gives concrete evidence of utility that is often missing from purely theoretical automata papers.

minor comments (2)
  1. [Experimental evaluation] The experimental tables would benefit from an explicit statement of the benchmark set (number and source of LTL formulas) and the precise timeout/memory limits used, so that the size and time comparisons can be reproduced.
  2. [Definition of VWAA unambiguity] A short worked example illustrating a VWAA that satisfies the new unambiguity definition but would be ambiguous under the classical notion would make the key technical distinction easier to follow.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, the recognition of the novelty of the VWAA-based route, and the recommendation for minor revision. The report correctly identifies the key elements of the paper: the new unambiguity notion for VWAA, the disambiguation procedure, the VWAA-level optimizations, the targeted LTL simplifications, the duggi implementation, and the experimental comparison with SPOT including the Markov-chain application.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper presents a new LTL-to-UBA construction that routes through VWAA using a novel unambiguity notion and disambiguation procedure, all introduced and defined within the work itself. It supplies the definitions, the procedure, optimizations, and experimental comparisons without reducing any central claim to a self-citation chain, fitted parameter renamed as prediction, or self-definitional equivalence. The derivation is self-contained against external benchmarks, with no load-bearing steps that collapse by construction to the inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review provides no information on free parameters, axioms, or invented entities.

pith-pipeline@v0.9.0 · 5678 in / 1149 out tokens · 29674 ms · 2026-05-25T01:36:47.445133+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages · 1 internal anchor

  1. [1]

    In: Automata on Infinite Words, Ecole de Printemps d’Informatique Th´ eorique, Le Mont Dore, May 1984

    Arnold, A.: Deterministic and non ambiguous rational ω-languages. In: Automata on Infinite Words, Ecole de Printemps d’Informatique Th´ eorique, Le Mont Dore, May 1984. Lecture Notes in Computer Science, vol. 192, pp. 18–27. Springer (1985)

    work page 1984

  2. [2]

    In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV)

    Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., Kˇ ret´ ınsk´ y, J., M¨ uller, D., Parker, D., Strejˇ cek, J.: The Hanoi omega-automata format. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 9206, pp. 479–486. Springer (2015)

    work page 2015

  3. [3]

    In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)

    Babiak, T., Kˇ ret´ ınsk´ y, M.,ˇReh´ ak, V., Strej˘ cek, J.: LTL to B¨ uchi automata trans- lation: Fast and more deterministic. In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 7214, pp. 95–109. Springer (2012)

    work page 2012

  4. [4]

    MIT Press (2008)

    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)

    work page 2008

  5. [5]

    In: Proceedings of the 28th International Conference on Computer Aided Verification (CAV) - Part I

    Baier, C., Kiefer, S., Klein, J., Kl¨ uppelholz, S., M¨ uller, D., Worrell, J.: Markov chains and unambiguous B¨ uchi automata. In: Proceedings of the 28th International Conference on Computer Aided Verification (CAV) - Part I. Lecture Notes in Computer Science, vol. 9779, pp. 23–42. Springer (2016)

    work page 2016

  6. [6]

    In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)

    Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 7795, pp. 32–46. Springer (2013)

    work page 2013

  7. [7]

    In: Proceedings of the 4th International Conference on Language and Automata Theory and Applications (LATA)

    Bousquet, N., L¨ oding, C.: Equivalence and inclusion problem for strongly un- ambiguous B¨ uchi automata. In: Proceedings of the 4th International Conference on Language and Automata Theory and Applications (LATA). Lecture Notes in Computer Science, vol. 6031, pp. 118–129. Springer (2010)

    work page 2010

  8. [8]

    Carton, O., Michel, M.: Unambiguous B¨ uchi automata. Theor. Comput. Sci.297(1- 3), 37–81 (2003)

    work page 2003

  9. [9]

    MIT Press (2001)

    Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (2001)

    work page 2001

  10. [10]

    In: Proceedings of the 17th International Workshop on Descriptional Complexity of Formal Systems (DCFS)

    Colcombet, T.: Unambiguity in automata theory. In: Proceedings of the 17th International Workshop on Descriptional Complexity of Formal Systems (DCFS). Lecture Notes in Computer Science, vol. 9118, pp. 3–18. Springer (2015)

    work page 2015

  11. [11]

    In: Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM)

    Couvreur, J.: On-the-fly verification of linear temporal logic. In: Proceedings of the World Congress on Formal Methods in the Development of Computing Systems (FM). Lecture Notes in Computer Science, vol. 1708, pp. 253–271. Springer (1999)

    work page 1999

  12. [12]

    In: Proceedings of the 10th International Con- ference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)

    Couvreur, J., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: Proceedings of the 10th International Con- ference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). Lecture Notes in Computer Science, vol. 2850, pp. 361–375. Springer (2003)

    work page 2003

  13. [13]

    In: Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA)

    Duret-Lutz, A.: Manipulating LTL formulas using Spot 1.0. In: Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 8172, pp. 442–445. Springer (2013)

    work page 2013

  14. [14]

    Habil- itation thesis, Universit´ e Pierre et Marie Curie (Paris 6) (Feb 2017)

    Duret-Lutz, A.: Contributions to LTL and ω-Automata for Model Checking. Habil- itation thesis, Universit´ e Pierre et Marie Curie (Paris 6) (Feb 2017)

    work page 2017

  15. [15]

    In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA)

    Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 — a framework for LTL and ω-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 9938, pp. 122–129. Springer (Oct 2016) From LTL to Unambiguous B...

    work page 2016

  16. [16]

    In: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR)

    Etessami, K., Holzmann, G.: Optimizing B¨ uchi automata. In: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 1877, pp. 153–167. Springer (2000)

    work page 2000

  17. [17]

    In: Proceedings of the 13th International Conference on Computer Aided Verification (CAV)

    Gastin, P., Oddoux, D.: Fast LTL to B¨ uchi automata translation. In: Proceedings of the 13th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2102, pp. 53–65. Springer (2001)

    work page 2001

  18. [18]

    In: Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification (PSTV)

    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verifica- tion of linear temporal logic. In: Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification (PSTV). IFIP Conference Proceedings, vol. 38, pp. 3–18. Chapman & Hall (1995)

    work page 1995

  19. [19]

    (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol

    Gr¨ adel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol. 2500. Springer (2002)

    work page 2002

  20. [20]

    In: 26th International Conference on Concur- rency Theory (CONCUR 2015)

    Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy Probabilistic Model Checking without Determinisation. In: 26th International Conference on Concur- rency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 42, pp. 354–367. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2015)

    work page 2015

  21. [21]

    In: 19th IEEE Symposium on Reliable Dis- tributed Systems (SRDS)

    Haverkort, B.R., Hermanns, H., Katoen, J.P.: On the use of model checking tech- niques for dependability evaluation. In: 19th IEEE Symposium on Reliable Dis- tributed Systems (SRDS). pp. 228–237. IEEE Computer Society (2000)

    work page 2000

  22. [22]

    Information Processing Letters 112(14-15), 578–582 (2012)

    Isaak, D., L¨ oding, C.: Efficient inclusion testing for simple classes of unambiguous ω-automata. Information Processing Letters 112(14-15), 578–582 (2012)

    work page 2012

  23. [23]

    In: Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA)

    Karmarkar, H., Joglekar, M., Chakraborty, S.: Improved upper and lower bounds for B¨ uchi disambiguation. In: Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA). pp. 40–54 (2013)

    work page 2013

  24. [24]

    LTL Store: Repository of LTL formulae from literature and case studies

    Kret´ ınsk´ y, J., Meggendorfer, T., Sickert, S.: LTL store: Repository of LTL formulae from literature and case studies. CoRR abs/1807.03296 (2018), http://arxiv. org/abs/1807.03296

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  25. [25]

    In: Proceedings of the 9th International Conference on Quantitative Evaluation of SysTems (QEST)

    Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of the 9th International Conference on Quantitative Evaluation of SysTems (QEST). pp. 203–204. IEEE Computer Society (2012)

    work page 2012

  26. [26]

    Information Processing Letters 79(3), 105–109 (2001)

    L¨ oding, C.: Efficient minimization of deterministic weakω-automata. Information Processing Letters 79(3), 105–109 (2001)

    work page 2001

  27. [27]

    In: Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics IFIP TCS

    L¨ oding, C., Thomas, W.: Alternating automata and logics over infinite words. In: Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics IFIP TCS. pp. 521–535 (2000)

    work page 2000

  28. [28]

    International Journal of Foundations of Computer Science 24(6), 847–862 (2013)

    Mohri, M.: On the disambiguation of finite automata and functional transducers. International Journal of Foundations of Computer Science 24(6), 847–862 (2013)

    work page 2013

  29. [29]

    In: Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF)

    M¨ uller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF). Electronic Proceedings in Theoretical Computer Science, vol. 256, pp. 180–194. Open Publishing Association (2017)

    work page 2017

  30. [30]

    In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS)

    Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS). pp. 422–427 (1988)

    work page 1988

  31. [31]

    Theoretical Computer Science 54, 267–276 (1987)

    Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theoretical Computer Science 54, 267–276 (1987)

    work page 1987

  32. [32]

    Journal of the ACM 32(3), 733–749 (1985) 18 Simon Jantsch et al

    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3), 733–749 (1985) 18 Simon Jantsch et al

    work page 1985

  33. [33]

    In: Proceed- ings of the 12th International Conference on Computer Aided Verification (CAV)

    Somenzi, F., Bloem, R.: Efficient B¨ uchi automata from LTL formulae. In: Proceed- ings of the 12th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 1855, pp. 248–263. Springer (2000)

    work page 2000

  34. [34]

    SIAM Journal on Computing pp

    Stearns, R.E., Hunt, H.B.: On the equivalence and containment problem for unam- biguous regular expressions, grammars, and automata. SIAM Journal on Computing pp. 598–611 (1985)

    work page 1985

  35. [35]

    In: Proceedings of the 26th IEEE Symposium on Foundations of Computer Science (FOCS)

    Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the 26th IEEE Symposium on Foundations of Computer Science (FOCS). pp. 327–338. IEEE Computer Society (1985)

    work page 1985

  36. [36]

    In: Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS)

    Vardi, M.Y.: Nontraditional applications of automata theory. In: Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS). pp. 575–597 (1994)

    work page 1994

  37. [37]

    In: Proceedings of the 1st Symposium on Logic in Computer Science (LICS)

    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the 1st Symposium on Logic in Computer Science (LICS). pp. 332–344. IEEE Computer Society Press (1986) From LTL to Unambiguous B¨ uchi Automata 19 A From LTL to VW AA We follow the translation given in [ 17] but use all subform...

    work page 1986

  38. [38]

    The first k failures occur on the first/left cluster

    ϕU(ν∨ ψ)≡ ν∨ γ and 2. L(ν)∩L (γ) = ∅ where γ = ϕU ((ϕ∧¬ g(ν)∧⃝ ν)∨ (ψ∧¬ ν)). Proof. We show 1. by showing ϕU(ν∨ ψ) =⇒ ν∨ γ and ν∨ γ =⇒ ϕU(ν∨ ψ). – ϕU(ν∨ ψ) =⇒ ν∨ γ: Take a word w that satisfies ϕU(ν∨ ψ). If w|= ν we are done. We know that either w|= ϕU ν or w|= ϕU ψ. In the first case there is a least i such that w[i..]|= ν and for all j < i : w[j..]|= ϕ. W...

    work page 2018