pith. machine review for the scientific record. sign in

arxiv: 2605.12372 · v1 · submitted 2026-05-12 · 💻 cs.FL · cs.LO

Recognition: no theorem link

Fast Obligation Translation and Synthesis

Alexandre Duret-Lutz, Giuseppe De Giacomo, Marcin Jurdzinski, Moshe Y. Vardi, Nir Piterman, Shufang Zhu

Authors on Pith no claims yet

Pith reviewed 2026-05-13 02:34 UTC · model grok-4.3

classification 💻 cs.FL cs.LO
keywords LTLsyntactic obligationsdeterministic weak automataMTBDDreactive synthesisomega-automataSpotformal verification
0
0 comments X

The pith

Syntactic obligations in LTL translate efficiently to minimal deterministic weak omega-automata encoded as multi-terminal binary decision diagrams, supporting direct on-the-fly synthesis.

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

The paper shows that a restricted class of linear temporal logic formulas called syntactic obligations convert directly into minimal deterministic weak automata. These automata are stored compactly using multi-terminal binary decision diagrams rather than explicit state graphs. Synthesis problems for such specifications can then be solved by operating on the diagram representation without first expanding it into a full automaton. This yields measurable speedups in both translation and synthesis steps inside the Spot library. A reader would care because obligation-style specifications appear often in reactive systems, and faster handling of them lowers the cost of automated controller design.

Core claim

Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak ω-automata. These can be converted very efficiently to minimal DWA represented using multi-terminal binary decision diagrams, and synthesis of such specifications can be solved directly on the MTBDD representation on the fly. The implementation in Spot demonstrates substantial runtime improvements in both translation and synthesis tasks.

What carries the argument

Multi-terminal binary decision diagram (MTBDD) encoding of the minimal deterministic weak omega-automaton obtained from a syntactic obligation formula; the diagram allows symbolic on-the-fly exploration during synthesis while retaining determinism and minimality.

If this is right

  • Translation of obligation formulas becomes fast enough for repeated use inside larger verification pipelines.
  • Synthesis no longer requires materializing the full state space of the automaton before search begins.
  • Minimal representations are obtained without post-processing minimization steps.
  • The same MTBDD structure supports both model checking and synthesis tasks for obligation specifications.

Where Pith is reading between the lines

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

  • The technique might extend to other LTL fragments whose automata are known to be deterministic and weak.
  • Direct diagram manipulation could reduce peak memory use in synthesis tools that currently expand automata explicitly.
  • Integration with existing symbolic engines may allow obligation synthesis to scale to larger state spaces than explicit methods permit.

Load-bearing premise

The MTBDD representation of the automaton from a syntactic obligation formula stays minimal and deterministic and introduces no hidden exponential blow-up when synthesis is performed directly on the diagram.

What would settle it

A syntactic obligation formula for which the MTBDD translation produces either a non-minimal automaton or a non-deterministic one, or for which on-the-fly synthesis returns an incorrect controller, would falsify the central claim.

Figures

Figures reproduced from arXiv: 2605.12372 by Alexandre Duret-Lutz, Giuseppe De Giacomo, Marcin Jurdzinski, Moshe Y. Vardi, Nir Piterman, Shufang Zhu.

Figure 1
Figure 1. Figure 1: A DBA for the formula φ1 = G(i1 ∨ Xi2) ↔ Go, and its MTBDD representation. of all propositions, so there are 2|P| of them, but to simplify the notations, we label the edges of the automaton by Boolean formulas (in this example, implicit conjunctions) that are satisfied by all the assignments that would normally label the edge. In Spot, this explicit representation of automata uses edges labeled by BDDs. In… view at source ↗
Figure 2
Figure 2. Figure 2: Four pipelines usable by ltl2tgba to translate a syntactic obligation: new-min, new, old-min, and old. The spot::translator class implements the dashed box. can be configured to use different approaches. The path old-min corresponds to the de￾fault behavior of Spot 2.14: after some simple syntactic simplifications, the formula is converted into a non-deterministic Buchi automaton using Couvreur’s translati… view at source ↗
Figure 3
Figure 3. Figure 3: Comparison of translation tools on 494 syntactic obligations from the literature. [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Comparison of the three configurations of [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The MTDWA from Figure 1, and its two-player game interpretation. Both also [PITH_FULL_IMAGE:figures/full_fig_p021_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Solving the example from Figure 1 as a game, while it is being constructed. [PITH_FULL_IMAGE:figures/full_fig_p022_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The resulting Mealy machine is then simplified using techniques described in [PITH_FULL_IMAGE:figures/full_fig_p023_7.png] view at source ↗
Figure 7
Figure 7. Figure 7: Strategy extracted from Figure 6, represented using MTBDDs, or as an incom [PITH_FULL_IMAGE:figures/full_fig_p024_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Execution times of the different configurations, on the parametric formulas listed in [PITH_FULL_IMAGE:figures/full_fig_p025_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Runtime comparisons over 184 non-scalable formulas from various sources. [PITH_FULL_IMAGE:figures/full_fig_p025_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Overview of ltlsynt’s architecture, taken from its documentation. ltlsynt (new synt.) SemML ltlsynt (new trans.) ltlsynt (old trans.) Strix SSyft 6MB 10MB 20MB 50MB 100MB 200MB 400MB 600MB 1 10 20 30 40 50 60 70 80 90 100 108 realizability tasks ranked by memory independently for each tool memory [PITH_FULL_IMAGE:figures/full_fig_p028_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Memory usage for the experiment of Figure 4. [PITH_FULL_IMAGE:figures/full_fig_p028_11.png] view at source ↗
read the original abstract

Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak $\omega$-automata (DWA). We show that syntactic obligations can be very efficiently converted to minimal DWA represented using multi-terminal binary decision diagrams (MTBDDs), and that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. Our implementation in Spot shows substantial runtime improvements in translation and synthesis.

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 / 0 minor

Summary. The paper claims that syntactic obligations, a fragment of LTL formulas, can be very efficiently converted to minimal deterministic weak ω-automata (DWA) represented using multi-terminal binary decision diagrams (MTBDDs). It further shows that synthesis of such specifications can be solved directly on the MTBDD representation on the fly. The approach is implemented in Spot and yields substantial runtime improvements in translation and synthesis.

Significance. If the claims hold, the work is significant for automata-based verification and reactive synthesis. It provides a compact MTBDD representation that preserves DWA minimality, determinism, and correctness while enabling on-the-fly synthesis without hidden exponential costs. The Spot implementation and reported performance gains offer practical value for handling common LTL obligation fragments at scale.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review and recommendation to accept the manuscript. We appreciate the recognition of the significance of our MTBDD-based approach for syntactic LTL obligations, including the preservation of minimality, determinism, and correctness, as well as the practical runtime gains demonstrated in Spot.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper describes an algorithmic procedure for translating syntactic obligations (a fragment of LTL) into minimal deterministic weak ω-automata represented via MTBDDs, followed by on-the-fly synthesis performed directly on that representation. No equations, definitions, or uniqueness claims are presented that reduce by construction to fitted inputs, self-referential parameters, or load-bearing self-citations; the contribution consists of explicit algorithmic steps and an implementation in Spot whose correctness and efficiency are asserted via construction and experimental validation rather than circular renaming or imported ansatzes. The derivation chain is therefore self-contained as a standard algorithmic result.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no mathematical derivations, parameters, or new entities are described, so the ledger is empty.

pith-pipeline@v0.9.0 · 5367 in / 1102 out tokens · 46724 ms · 2026-05-13T02:34:00.985758+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

87 extracted references · 87 canonical work pages

  1. [1]

    In: Proceedings of the 33rd International Conference on Computer Aided Verification (CA V’21)

    Amram, G., Bansal, S., Fried, D., Tabajara, L.M., Vardi, M.Y ., Weiss, G.: Adapting behaviors via reactive synthesis. In: Proceedings of the 33rd International Conference on Computer Aided Verification (CA V’21). pp. 870–89. Springer International Publishing (2021). https: //doi.org/10.1007/978-3-030-81685-8 41

    work page doi:10.1007/978-3-030-81685-8 2021

  2. [2]

    In: Proceedings of the 27th International Conference on Computer Aided Verification (CA V’15)

    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 (CA V’15). Lecture Notes in Computer Science, vol. 9206, pp. 479–486. Springer (Jul 2015). https://doi.org/10.1007/978-3-319-2...

    work page doi:10.1007/978-3-319-21690-4 2015

  3. [3]

    In: Lal, A., Tonetta, S

    Bansal, S., De Giacomo, G., Di Stasio, A., Li, Y ., Vardi, M.Y ., Zhu, S.: Compositional safety LTL synthesis. In: Lal, A., Tonetta, S. (eds.) Proceedings of the 14th International Confer- ence on Verified Software, Theories, Tools and Experiments (VSTTE’22). pp. 1–19. Springer International Publishing (2023). https://doi.org/10.1007/978-3-031-25803-9 1

    work page doi:10.1007/978-3-031-25803-9 2023

  4. [4]

    In: Proceedings of the 34th national conference on Artificial intelligence (AAAI’20)

    Bansal, S., Li, Y ., Tabajara, L.M., Vardi, M.Y .: Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: Proceedings of the 34th national conference on Artificial intelligence (AAAI’20). pp. 9766–9774. AAAI Press (2020). https://doi.org/10. 1609/AAAI.V34I06.6528

    work page 2020

  5. [5]

    In- ternational Journal on Software Tools for Technology Transfer21, 1–29 (Feb 2019)

    Beyer, D., L ¨owe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. In- ternational Journal on Software Tools for Technology Transfer21, 1–29 (Feb 2019). https: //doi.org/10.1007/s10009-017-0469-y

    work page doi:10.1007/s10009-017-0469-y 2019

  6. [6]

    Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011), https://fmv.jku.at/aiger/

    work page 2011

  7. [7]

    Journal of Computer and System Sciences78(3), 911–938 (2012)

    Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y .: Synthesis of reactive(1) de- signs. Journal of Computer and System Sciences78(3), 911–938 (2012). https://doi.org/10. 1016/J.JCSS.2011.08.007

    work page 2012

  8. [8]

    IEEE Transactions on Computers35(8), 677–691 (Aug 1986)

    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers35(8), 677–691 (Aug 1986). https://doi.org/10.1109/TC.1986.1676819

    work page doi:10.1109/tc.1986.1676819 1986

  9. [9]

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

    Casares, A., Duret-Lutz, A., Meyer, K.J., Renkin, F., Sickert, S.: Practical applications of the Alternating Cycle Decomposition. In: Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’22). Lecture Notes in Computer Science, vol. 13244, pp. 99–117 (Apr 2022). https://doi.org/10.1007...

    work page 2022

  10. [10]

    In: Rovan, B., V ojt´aˇa, P

    ˇCern´a, I., Pel ´anek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., V ojt´aˇa, P. (eds.) Proceedings of the 28th International Symposium on Math- ematical Foundations of Computer Science (MFCS’03). Lecture Notes in Computer Sci- ence, vol. 2747, pp. 318–327. Springer-Verlag, Bratislava, Slovak Republic (Aug 2003). https...

    work page doi:10.1007/978-3-540-45138-9 2003

  11. [11]

    In: Pro- ceedings of the 19th International Colloquium on Automata, Languages and Programming (ICALP’92)

    Chang, E.Y ., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Pro- ceedings of the 19th International Colloquium on Automata, Languages and Programming (ICALP’92). pp. 474–486. Springer-Verlag, London, UK (1992). https://doi.org/10.1007/ 3-540-55719-9 97

    work page 1992

  12. [12]

    Chatterjee, K.: Linear time algorithm for weak parity games. Tech. Rep. UCB/EECS-2006- 153, Electrical Engineering and Computer Sciences, University of California at Berkeley (Nov 2008), https://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-153.html Fast Obligation Translation and Synthesis 13

    work page 2006

  13. [13]

    In: Proceedings of the Fourth International Conference on Dependability of Com- puter Systems (DepCoS’09)

    Cicho ´n, J., Czubak, A., Jasi ´nski, A.: Minimal B ¨uchi automata for certain classes of LTL formulas. In: Proceedings of the Fourth International Conference on Dependability of Com- puter Systems (DepCoS’09). pp. 17–24. IEEE Computer Society (2009). https://doi.org/10. 1109/DepCoS-RELCOMEX.2009.31

    work page 2009

  14. [14]

    In: Wing, J.M., Woodcock, J., Davies, J

    Couvreur, J.M.: On-the-fly verification of temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) Proceedings of the World Congress on Formal Methods in the Develop- ment of Computing Systems (FM’99). Lecture Notes in Computer Science, vol. 1708, pp. 253–271. Springer-Verlag (Sep 1999). https://doi.org/10.1007/3-540-48119-2 16

    work page doi:10.1007/3-540-48119-2 1999

  15. [15]

    In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y

    Dax, C., Eisinger, J., Klaedtke, F.: Mechanizing the powerset construction for restricted classes ofω-automata. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y . (eds.) Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATV A’07). Lecture Notes in Computer Science, vol. 4762. Springer-Verlag (Oc...

    work page doi:10.1007/978-3-540-75596-8 2007

  16. [16]

    In: Proceedings of the 31st International Conference on Automated Planning and Scheduling (ICAPS’21)

    De Giacomo, G., Favorito, M.: Compositional approach to translate LTL f /LDL f into deter- ministic finite automata. In: Proceedings of the 31st International Conference on Automated Planning and Scheduling (ICAPS’21). pp. 122–130 (2021). https://doi.org/10.1609/icaps. v31i1.15954

    work page doi:10.1609/icaps 2021

  17. [17]

    In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJ- CAI’13)

    De Giacomo, G., Vardi, M.Y .: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJ- CAI’13). pp. 854–860. AAAI Press (Aug 2013). https://doi.org/10.5555/2540128.2540252

    work page doi:10.5555/2540128.2540252 2013

  18. [18]

    In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15)

    De Giacomo, G., Vardi, M.Y .: Synthesis for LTL and LDL on finite traces. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI’15). pp. 1558–1564. AAAI Press (2015). https://doi.org/10.5555/2832415.2832466

    work page doi:10.5555/2832415.2832466 2015

  19. [19]

    http://www.cs.utexas.edu/users/EWD/ewd03xx/EWD376.PDF (May 1973)

    Dijkstra, E.W.: EWD 376: Finding the maximum strong components in a directed graph. http://www.cs.utexas.edu/users/EWD/ewd03xx/EWD376.PDF (May 1973)

    work page 1973

  20. [20]

    In: A Discipline of Programming, chap

    Dijkstra, E.W.: Finding the maximal strong components in a directed graph. In: A Discipline of Programming, chap. 25, pp. 192–200. Prentice-Hall (1976)

    work page 1976

  21. [21]

    International Journal on Critical Computer-Based Systems5(1/2), 31–54 (Mar 2014)

    Duret-Lutz, A.: LTL translation improvements in Spot 1.0. International Journal on Critical Computer-Based Systems5(1/2), 31–54 (Mar 2014). https://doi.org/10.1504/IJCCBS.2014. 059594

    work page doi:10.1504/ijccbs.2014 2014

  22. [22]

    https://doi.org/10.5281/zenodo.19812382

    Duret-Lutz, A.: Supporting material for ”Fast Obligation Translation and Synthesis” (Jan 2026). https://doi.org/10.5281/zenodo.19812382

    work page doi:10.5281/zenodo.19812382 2026

  23. [23]

    Lecture Notes in Computer Science, vol

    Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From Spot 2.0 to Spot 2.10: What’s new? In: Proceedings of the 34th International Conferencermane on Computer Aided Verification (CA V’22). Lecture Notes in Computer Science, vol. 13372, pp. 174–187. Spri...

    work page doi:10.1007/978-3-031-13188-2 2022

  24. [24]

    In: Proceedings of the 29th International Conference on Implementation and Applications of Automata (CIAA’25)

    Duret-Lutz, A., Zhu, S., Piterman, N., De Giacomo, G., Vardi, M.Y .: Engineering an LTLf synthesis tool. In: Proceedings of the 29th International Conference on Implementation and Applications of Automata (CIAA’25). Lecture Notes in Computer Science, vol. 15981, pp. 129–147. Springer (Sep 2025). https://doi.org/10.1007/978-3-032-02602-6 10

    work page doi:10.1007/978-3-032-02602-6 2025

  25. [25]

    In: Ardis, M

    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Ardis, M. (ed.) Proceedings of the 2nd Workshop on Formal Methods in Software Practice (FMSP’98). pp. 7–15. ACM Press (Mar 1998). https://doi.org/10.1145/ 298595.298598

    work page arXiv 1998

  26. [26]

    In: Dawar, A., Gr ¨adel, E

    Esparza, J., K ˇret´ınsk´y, J., Sickert, S.: One theorem to rule them all: A unified translation of LTL intoω-automata. In: Dawar, A., Gr ¨adel, E. (eds.) Proceedings of the 33rd An- nual ACM/IEEE Symposium on Logic in Computer Science (LICS’18). pp. 384–393. ACM (2018). https://doi.org/10.1145/3209108.3209161

    work page doi:10.1145/3209108.3209161 2018

  27. [27]

    Journal of the ACM71(2) (Apr 2024)

    Esparza, J., Rubio, R., Sickert, S.: Efficient normalization of linear temporal logic. Journal of the ACM71(2) (Apr 2024). https://doi.org/10.1145/3651152 14 A. Duret-Lutz et al

    work page doi:10.1145/3651152 2024

  28. [28]

    In: Palamidessi, C

    Etessami, K., Holzmann, G.J.: Optimizing B ¨uchi automata. In: Palamidessi, C. (ed.) Pro- ceedings of the 11th International Conference on Concurrency Theory (Concur’00). Lecture Notes in Computer Science, vol. 1877, pp. 153–167. Springer-Verlag, Pennsylvania, USA (2000). https://doi.org/10.1007/3-540-44618-4 13

    work page doi:10.1007/3-540-44618-4 2000

  29. [29]

    In: Javier Esparza, Orna Grumberg, S.S

    Finkbeiner, B.: Synthesis of reactive systems. In: Javier Esparza, Orna Grumberg, S.S. (ed.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series — D: Information and Communication Security, vol. 45, pp. 72–98. IOS Press (2016). https: //doi.org/10.3233/978-1-61499-627-9-72

    work page doi:10.3233/978-1-61499-627-9-72 2016

  30. [30]

    In: Proceedings for the 13th NASA Formal Methods Symposium (NFM’21)

    Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis. In: Proceedings for the 13th NASA Formal Methods Symposium (NFM’21). Lecture Notes in Computer Science, vol. 12673, pp. 113–130. Springer (2021). https://doi.org/10.1007/ 978-3-030-76384-8 8

    work page 2021

  31. [31]

    Formal Methods in System Design10(2/3), 149–169 (1997)

    Fujita, M., McGeer, P.C., Yang, J.C.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design10(2/3), 149–169 (1997). https://doi.org/10.1023/A:1008647823331

    work page doi:10.1023/a:1008647823331 1997

  32. [32]

    In: Hlinen ´y, P., Maty´as, V ., V ojnar, T

    Gaiser, A., Schwoon, S.: Comparison of algorithms for checking emptiness on B ¨uchi au- tomata. In: Hlinen ´y, P., Maty´as, V ., V ojnar, T. (eds.) Procedings of Annual Doctoral Work- shop on Mathematical and Engineering Methods in Computer Science (MEMICS’09). OA- SICS, vol. 13. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, Germany (Nov 2009). https...

    work page doi:10.4230/drops.memics.2009.2349 2009

  33. [33]

    In: Proceedings of the 13th International SPIN Workshop (SPIN’06)

    Geldenhuys, J., Hansen, H.: Larger automata and less work for LTL model checking. In: Proceedings of the 13th International SPIN Workshop (SPIN’06). Lecture Notes in Computer Science, vol. 3925, pp. 53–70. Springer (2006). https://doi.org/10.1007/11691617 4

    work page doi:10.1007/11691617 2006

  34. [34]

    Pattern Recog- nition153, 110500 (2024).https://doi.org/https://doi.org/10.1016/j

    Geldenhuys, J., Valmari, A.: More efficient on-the-fly LTL verification with Tarjan’s algo- rithm. Theoretical Computer Science345(1), 60–82 (Nov 2005). https://doi.org/10.1016/j. tcs.2005.07.004

    work page doi:10.1016/j 2005

  35. [35]

    In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B

    Henriksen, J.G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’95). pp. 89–110. Springer Ber...

    work page doi:10.1007/3-540-60630-0 1995

  36. [36]

    Hole ˇcek, J., Kratochv ´ıla, T., ˇReh´ak, V ., ˇSafr´anek, D., ˇSimeˇcek, P.: Verification results in Liberouter project. Tech. Rep. 03, CESNET (September 2004), http://archiv.cesnet.cz/doc/ techzpravy/2004/verificationresults/

    work page 2004

  37. [37]

    arXiV (Jun 2022)

    Jacobs, S., Perez, G.A., Abraham, R., Bruy `ere, V ., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Lut- tenberger, M., Meyer, K.J., Michaud, T., Pommellet, A., Renkin, F., Schlehuber-Caissier, P., Sakr, M., Sickert, S., Staquet, G., Tamines, C., Tentrup, L., Walker, A.: Th...

    work page arXiv 2018

  38. [38]

    Klarlund, N., Møller, A.:MONAversion 1.4, user manual. Tech. rep., BRICS (Jul 2001), https://www.brics.dk/mona/mona14.pdf

    work page 2001

  39. [39]

    28 Kenneth L

    K ˇret´ınsk´y, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: SemML: Enhancing automata- theoretic LTL synthesis with machine learning. In: Gurfinkel, A., Heule, M. (eds.) Proceed- ings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’25). pp. 233–253. Springer Nature Switzerland (2025). http...

    work page doi:10.1007/978-3-031-90643-5 2025

  40. [40]

    In: Proceedings of the 16th International Symposium on Automated Technology for Verifica- tion and Analysis (ATV A’18)

    Kret ´ınsk´y, J., Meggendorfer, T., Sickert, S.: Owl: A library forω-words, automata, and LTL. In: Proceedings of the 16th International Symposium on Automated Technology for Verifica- tion and Analysis (ATV A’18). Lecture Notes in Computer Science, vol. 11138, pp. 543–550. Springer (2018). https://doi.org/10.1007/978-3-030-01090-4 34 Fast Obligation Tran...

    work page doi:10.1007/978-3-030-01090-4 2018

  41. [41]

    In: van der Meyden, R., Smaus, J.G

    Kupferman, O., Rosenberg, A.: The blow-up in translating ltl to deterministic automata. In: van der Meyden, R., Smaus, J.G. (eds.) Proceedings of the 6th International Workshop on Model Checking and Artificial Intelligence (MochArt’11). pp. 85–94. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20674-0 6

    work page doi:10.1007/978-3-642-20674-0 2011

  42. [42]

    In: Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS’05)

    Kupferman, O., Vardi, M.Y .: Safraless decision procedures. In: Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS’05). pp. 531–542 (2005). https://doi.org/10.1109/SFCS.2005.66

    work page doi:10.1109/sfcs.2005.66 2005

  43. [43]

    Journal of the ACM47(2), 312–360 (Mar 2000)

    Kupferman, O., Vardi, M.Y ., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM47(2), 312–360 (Mar 2000). https://doi.org/10.1145/ 333979.333987

    work page arXiv 2000

  44. [44]

    In: Proceedings of the 28th European Conference on Artificial Intelligence (ECAI’25)

    Li, Y ., Xiao, S., Zhu, S., Li, J., Pu, G.: A compositional framework for on-the-fly LTL f synthesis. In: Proceedings of the 28th European Conference on Artificial Intelligence (ECAI’25). pp. 1711–1718. Frontiers in Artificial Intelligence and Applications (2025). https://doi.org/10.3233/FAIA250999

    work page doi:10.3233/faia250999 2025

  45. [45]

    L ¨oding, C.: Methods for the Transformation ofω-Automata: Complexity and Connection to Second Order Logic. Diploma thesis, Institute of Computer Science and Applied Mathemat- ics Christian-Albrechts-University of Kiel (1998), https://www.lics.rwth-aachen.de/global/ show document.asp?id=aaaaaaaaabcqdty

    work page 1998

  46. [46]

    Information Process- ing Letters79(3), 105–109 (2001)

    L ¨oding, C.: Efficient minimization of deterministic weakω-automata. Information Process- ing Letters79(3), 105–109 (2001). https://doi.org/10.1016/S0020-0190(00)00183-6

    work page doi:10.1016/s0020-0190(00)00183-6 2001

  47. [47]

    source archive, https://www.cs.cmu.edu/ ∼modelcheck/bdd.html

    Long, D.: BDD library. source archive, https://www.cs.cmu.edu/ ∼modelcheck/bdd.html

    work page

  48. [48]

    Acta Informatica57(1-2), 3–36 (2020)

    Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica57(1-2), 3–36 (2020). https://doi.org/10. 1007/S00236-019-00349-3

    work page 2020

  49. [49]

    In: Proceedings of the 17th Inter- national Symposium on Automated Technology for Verification and Analysis (ATV A’19)

    Major, J., Blahoudek, F., Strejcek, J., Sasar ´akov´a, M., Zbonc´akov´a, T.: ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In: Proceedings of the 17th Inter- national Symposium on Automated Technology for Verification and Analysis (ATV A’19). Lecture Notes in Computer Science, vol. 11781, pp. 357–365 (2019). https://doi.or...

    work page 2019

  50. [50]

    In: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing (PODC’90)

    Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing (PODC’90). pp. 377–410. ACM, New York, NY , USA (1990). https://doi.org/10.1145/93385.93442

    work page doi:10.1145/93385.93442 1990

  51. [51]

    Springer (1992)

    Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: Specification. Springer (1992). https://doi.org/10.1007/978-1-4612-0931-7

    work page doi:10.1007/978-1-4612-0931-7 1992

  52. [52]

    Springer (1995)

    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. Springer (1995). https://doi.org/10.1007/978-1-4612-4222-2

    work page doi:10.1007/978-1-4612-4222-2 1995

  53. [53]

    In: Manna, Z., Peled, D.A

    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Response. In: Manna, Z., Peled, D.A. (eds.) Time for Verification: Essays in Memory of Amir Pnueli, Lecture Notes in Computer Science, vol. 6200, pp. 279–361. Springer (2010). https://doi.org/10. 1007/978-3-642-13754-9 13

    work page 2010

  54. [54]

    Minato, S.i.: Representation of Multi-Valued Functions, pp. 39–47. Springer US, Boston, MA (1996). https://doi.org/10.1007/978-1-4613-1303-8 4

    work page doi:10.1007/978-1-4613-1303-8 1996

  55. [55]

    In: Automata studies, pp

    Moore, E.F.: Gedanken-experiments on sequential machines. In: Automata studies, pp. 129–

    work page

  56. [56]

    34 in Annals of Mathematical Studies, Princeton University Press (1956)

    No. 34 in Annals of Mathematical Studies, Princeton University Press (1956)

    work page 1956

  57. [57]

    In: Proceedings of the 8th International Sumposium on Games, Automata, Logics and Formal Verification (Gan- dALF’17)

    M ¨uller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Proceedings of the 8th International Sumposium on Games, Automata, Logics and Formal Verification (Gan- dALF’17). Electronic Proceedings in Theoretical Computer Science, vol. 256, pp. 180–194. Open Publishing Association (2017). https://doi.org/10.4204/EPTCS.256.13

    work page doi:10.4204/eptcs.256.13 2017

  58. [58]

    In: Proceedings of the 14th international SPIN conference on Model checking software (Spin’07)

    Pel ´anek, R.: BEEM: benchmarks for explicit model checkers. In: Proceedings of the 14th international SPIN conference on Model checking software (Spin’07). Lecture Notes in 16 A. Duret-Lutz et al. Computer Science, vol. 4595, pp. 263–267. Springer-Verlag (2007). https://doi.org/10.1007/ 978-3-540-73370-6 17

    work page 2007

  59. [59]

    In: Proceedings of the 7th international conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06)

    Piterman, N., Pnueli, A., Sa’ar, Y .: Synthesis of reactive(1) designs. In: Proceedings of the 7th international conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06). Lecture Notes in Computer Science, vol. 3855, pp. 364–380. Springer (2006). https://doi.org/10.1007/11609773 24

    work page doi:10.1007/11609773 2006

  60. [60]

    In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS’77)

    Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS’77). pp. 46–57 (1977). https://doi.org/10.1109/ SFCS.1977.32

    work page 1977

  61. [61]

    In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL’89)

    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL’89). Association for Computing Machinery (1989). https://doi.org/10.1145/75277.75293

    work page doi:10.1145/75277.75293 1989

  62. [62]

    Fundamenta Informaticae119(3-4), 393–406 (2012)

    Redziejowski, R.: An improved construction of deterministic omega-automaton using derivatives. Fundamenta Informaticae119(3-4), 393–406 (2012). https://doi.org/10.3233/ FI-2012-744

    work page 2012

  63. [63]

    In: McMillan, K., Middeldorp, A., V oronkov, A

    Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Three SCC-based emptiness checks for generalized B¨uchi automata. In: McMillan, K., Middeldorp, A., V oronkov, A. (eds.) Pro- ceedings of the 19th International Conference on Logic for Programming, Artificial Intelli- gence, and Reasoning (LPAR-19). Lecture Notes in Computer Science, vol. 8312, pp. 668–

    work page

  64. [64]

    https://doi.org/10.1007/978-3-642-45221-5 44

    Springer (Dec 2013). https://doi.org/10.1007/978-3-642-45221-5 44

    work page doi:10.1007/978-3-642-45221-5 2013

  65. [65]

    paritizing

    Renkin, F., Duret-Lutz, A., Pommellet, A.: Practical “paritizing” of emerson-lei automata. In: Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATV A’20). Lecture Notes in Computer Science, vol. 12302, pp. 127–143. Springer (Oct 2020). https://doi.org/10.1007/978-3-030-59152-6 7

    work page doi:10.1007/978-3-030-59152-6 2020

  66. [66]

    In: Proceedings of the 42nd International Conference on Formal Tech- niques for Distributed Objects, Components, and Systems (FORTE’22)

    Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Effective reductions of Mealy machines. In: Proceedings of the 42nd International Conference on Formal Tech- niques for Distributed Objects, Components, and Systems (FORTE’22). Lecture Notes in Computer Science, vol. 13273, pp. 170–187. Springer (Jun 2022). https://doi.org/10.1007/ 978-3-...

    work page 2022

  67. [67]

    Formal Methods in System Design (2023)

    Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Dissectingltlsynt. Formal Methods in System Design (2023). https://doi.org/10.1007/s10703-022-00407-6

    work page doi:10.1007/s10703-022-00407-6 2023

  68. [68]

    Schewe, S.: Beyond hyper-minimisation—minimising DBAs and DPAs is NP-complete

    work page

  69. [69]

    In: Proceedings of the 12th International Conference on Computer Aided Verification (CA V’00)

    Somenzi, F., Bloem, R.: Efficient B¨uchi automata for LTL formulae. In: Proceedings of the 12th International Conference on Computer Aided Verification (CA V’00). Lecture Notes in Computer Science, vol. 1855, pp. 247–263. Springer-Verlag, Chicago, Illinois, USA (2000). https://doi.org/10.1007/10722167 21

    work page doi:10.1007/10722167 2000

  70. [70]

    In: Proceedings of the 1st International Conference on Runtime Verification (RV’10)

    Tabakov, D., Vardi, M.Y .: Optimized temporal monitors for SystemC. In: Proceedings of the 1st International Conference on Runtime Verification (RV’10). Lecture Notes in Computer Science, vol. 6418, pp. 436–451. Springer (Nov 2010). https://doi.org/10.1007/ 978-3-642-16612-9 33

    work page 2010

  71. [71]

    In: 26th Annual Symposium on Foundations of Computer Science (SFCS 1985)

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

    work page 1985

  72. [72]

    property class

    Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y .: Symbolic LTLf synthesis. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI’17). pp. 1362– 1369 (2017). https://doi.org/10.24963/ijcai.2017/189 Fast Obligation Translation and Synthesis 17 property classes syntactic classes source set sizeO O\S\G S\B G\B B O O...

    work page doi:10.24963/ijcai.2017/189 2017

  73. [73]

    translateφinto a non-deterministic B ¨uchi automatonN φ,

    work page

  74. [74]

    ignoring the acceptance of states, use the powerset construction onN φ to obtain the deterministicstructure D φ,

    work page

  75. [75]

    any SCC ofD φ that intersects an accepting SCC ofN φ in the synchronous product ofN φ ⊗D φ should be marked inD φ as fully accepting

    work page

  76. [76]

    at this pointD φ is a DW A such thatL(φ)⊆L(D φ) (because its accepting SCCs possibly capture runs that were not accepted byN φ)

    work page

  77. [77]

    The success of the last inclusion check implies thatL(D φ)=L(φ)

    testL(D φ)⊆L(φ) by constructing a non-deterministic B ¨uchi automatonN ¬φ for the negation ofφand then ensuring that the productN ¬φ ⊗D φ is empty. The success of the last inclusion check implies thatL(D φ)=L(φ). SinceD φ is a DW A, this in turn implies thatφis an obligation. After minimizing this DW A, we can also detect guarantee properties (the only ac...

    work page

  78. [78]

    If a stateφ∈ Qis such thatλ(φ)=∗, this state belongs to a trivial SCC of D ι

    work page

  79. [79]

    For any bottom formulaι∈LTL B(P), the only possible non-trivial SCCs of D ι are the states tt andff(at least one of these has to exist)

    work page

  80. [80]

    For any guarantee formulaι∈LTL G(P), all statesφ∈ Q \ {tt}that belong to non-trivial SCCs of Dι haveλ(φ)=⊥

    work page

Showing first 80 references.