pith. sign in

arxiv: 2604.24102 · v1 · submitted 2026-04-27 · 💻 cs.AI · cs.FL· cs.LO

SemML 2.0: Synthesizing Controllers for LTL

Jan K\v{r}et\'insk\'y , Tobias Meggendorfer , Maximilian Prokop This is my paper

Pith reviewed 2026-05-08 03:44 UTC · model grok-4.3

classification 💻 cs.AI cs.FLcs.LO
keywords LTL synthesisreactive controllersMealy machinesAIGER circuitsmachine learning guidancepartial explorationSYNTCOMP benchmarksautomata-theoretic synthesis
0
0 comments X

The pith

SemML 2.0 solves more LTL synthesis problems faster than existing tools while producing solutions of comparable size.

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

The paper presents an updated tool that turns specifications written in linear temporal logic into reactive controllers, represented either as Mealy machines or as circuits. It starts from the standard method of building automata from the logic formula but adds partial exploration of the state space and machine-learning predictions to steer the search toward solutions quickly. Heuristics then prune the results down to compact representations. On the standard collection of benchmark problems used in the synthesis competition, the new version finds answers for more cases and finishes them in less time than the leading prior tools, without degrading the quality of the controllers it returns.

Core claim

SemML 2.0 implements the classical automata-theoretic approach to LTL synthesis augmented with partial exploration and machine-learning guidance for efficient solution finding, along with heuristics to extract small Mealy machines or AIGER circuits, and demonstrates superior performance on SYNTCOMP benchmarks by solving more instances faster than state-of-the-art tools.

What carries the argument

Partial state-space exploration guided by machine learning, combined with heuristics for compact solution extraction inside the automata-theoretic LTL synthesis pipeline.

If this is right

  • A larger fraction of practical LTL synthesis tasks finish within ordinary time and memory limits.
  • Designers of safety-critical reactive systems can iterate on specifications more rapidly.
  • The same combination of partial search and learned guidance can be applied to other temporal-logic synthesis problems.
  • Compact controller representations remain competitive, so downstream verification and implementation steps are unaffected.
  • Faster synthesis supports repeated refinement loops inside larger engineering workflows.

Where Pith is reading between the lines

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

  • If the learned guidance generalizes across formula families, future tools may need fewer hand-crafted heuristics.
  • Partial exploration could scale to synthesis problems whose full automata are too large to build explicitly.
  • The performance pattern suggests that similar hybrids might help in related areas such as controller repair or assume-guarantee synthesis.
  • Wider adoption would make LTL-based controller generation a routine step rather than a research-only technique.

Load-bearing premise

The SYNTCOMP benchmark set accurately reflects the difficulty and structure of real-world LTL synthesis problems, and the reported speed and coverage gains are not due to tuning specific to those benchmarks.

What would settle it

Running SemML 2.0 and the competing tools on a fresh collection of LTL specifications taken from industrial control systems and observing that the advantage in solved instances or runtime disappears.

Figures

Figures reproduced from arXiv: 2604.24102 by Jan K\v{r}et\'insk\'y, Maximilian Prokop, Tobias Meggendorfer.

Figure 1
Figure 1. Figure 1: Structural overview of SemML’s high-level architecture. All items marked by + are novel or significant improvements over our prior version. Additionally, several minor engineering improvements have been added to all stages. High-level architecture. SemML solves LTL Synthesis via the automaton￾theoretic approach [37]. Here, the formula is first translated into an equivalent automaton (typically a parity aut… view at source ↗
Figure 4
Figure 4. Figure 4: DPA for the intersection of the DELA AE and the conditional Zielonka Tree. 20 view at source ↗
Figure 5
Figure 5. Figure 5: Confusion matrices to highlight unique and overlapping solves for every view at source ↗
Figure 6
Figure 6. Figure 6: Pairwise scatterplots to compare the solve times of two tools on a bench view at source ↗
Figure 7
Figure 7. Figure 7: Speedup factors for all tracks when taking different lower cutoffs. The view at source ↗
Figure 8
Figure 8. Figure 8: Pairwise scatterplots to compare the solution sizes of two tools on a bench view at source ↗
read the original abstract

Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.

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

3 major / 1 minor

Summary. The paper presents SemML 2.0 for synthesizing reactive controllers from LTL specifications, represented as Mealy machines or AIGER circuits. It augments the classical automata-theoretic approach with partial exploration, machine-learning guidance, and heuristics for compact solutions. On the SYNTCOMP benchmark, the tool is claimed to solve significantly more instances faster than Strix, LtlSynt, and the prior SemML version while maintaining state-of-the-art solution quality.

Significance. If the reported gains are robust, this would constitute a practical advance in LTL synthesis for safety-critical systems by showing how ML-guided partial search scales on standard benchmarks. The combination of classical methods with targeted ML and heuristics is a constructive contribution, and the use of the established SYNTCOMP suite provides a reproducible point of comparison.

major comments (3)
  1. [Abstract] Abstract: the claim that the tool solves 'significantly more instances' and 'much faster' than competitors is asserted without any quantitative tables, exact counts, runtime distributions, error bars, or statistical tests. This prevents assessment of the central empirical result.
  2. [Machine Learning Guidance] Machine Learning Guidance section: no statement confirms that the training corpus for the ML component is disjoint from the SYNTCOMP instances used for evaluation. Overlap would make the coverage gains non-generalizable and attributable to data leakage rather than the partial-exploration pipeline.
  3. [Experimental Evaluation] Experimental Evaluation: the manuscript supplies no information on whether all tools (including Strix and LtlSynt) were executed under identical timeout, memory, and hardware constraints. Without this, speed advantages cannot be confidently attributed to the described methods.
minor comments (1)
  1. [Introduction] Ensure all acronyms (LTL, AIGER, Mealy) are defined on first use and used consistently.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. The comments highlight important aspects of clarity and rigor in presenting our empirical results and experimental setup. We address each major comment point by point below, indicating the revisions we will make.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the tool solves 'significantly more instances' and 'much faster' than competitors is asserted without any quantitative tables, exact counts, runtime distributions, error bars, or statistical tests. This prevents assessment of the central empirical result.

    Authors: The abstract summarizes the key outcomes at a high level, while the Experimental Evaluation section contains the supporting tables with exact instance counts, runtime comparisons, and solution quality metrics against Strix, LtlSynt, and SemML 1.0. We agree that the abstract would be strengthened by including specific quantitative highlights. We will revise the abstract to incorporate key figures (e.g., number of additional instances solved and runtime speedups) drawn directly from the results. Since the underlying algorithms are deterministic, error bars are not applicable; we will instead ensure the full runtime data is clearly tabulated in the main text. revision: yes

  2. Referee: [Machine Learning Guidance] Machine Learning Guidance section: no statement confirms that the training corpus for the ML component is disjoint from the SYNTCOMP instances used for evaluation. Overlap would make the coverage gains non-generalizable and attributable to data leakage rather than the partial-exploration pipeline.

    Authors: The training corpus for the machine-learning guidance was generated from a separate collection of LTL specifications that does not intersect with the SYNTCOMP benchmark instances used in evaluation. This separation was deliberate to support generalizability. We will add an explicit statement in the Machine Learning Guidance section confirming the disjoint training and evaluation sets. revision: yes

  3. Referee: [Experimental Evaluation] Experimental Evaluation: the manuscript supplies no information on whether all tools (including Strix and LtlSynt) were executed under identical timeout, memory, and hardware constraints. Without this, speed advantages cannot be confidently attributed to the described methods.

    Authors: All tools were executed under identical conditions on the same hardware using the official implementations and the timeout/memory limits defined by the SYNTCOMP competition. We will expand the Experimental Evaluation section to document the precise hardware specifications, timeout values, memory limits, and confirmation that competitors ran under matching constraints. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical tool comparison on external benchmarks

full rationale

The paper presents SemML 2.0, an LTL synthesis tool using automata-theoretic methods augmented by partial exploration, ML guidance, and heuristics for small solutions. Its claims consist of direct empirical measurements of coverage, runtime, and solution quality on the SYNTCOMP benchmark set against independent external tools (Strix, LtlSynt, prior SemML). No mathematical derivations, equations, or first-principles results are offered that reduce any performance claim to a fitted parameter, self-defined quantity, or self-citation chain. The evaluation is externally falsifiable via re-running the tools on the public benchmark under stated conditions. Self-reference to the prior SemML version is incidental and not load-bearing for the new results.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities are described in the abstract; the work is an empirical engineering contribution rather than a theoretical derivation.

pith-pipeline@v0.9.0 · 5463 in / 1003 out tokens · 41045 ms · 2026-05-08T03:44:04.878629+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

46 extracted references · 25 canonical work pages

  1. [1]

    In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015, Austin, TX, USA, November 2-6, 2015

    Abel, A., Reineke, J.: Memin: Sat-based exact minimization of incompletely specified mealy machines. In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015, Austin, TX, USA, November 2-6, 2015. pp. 94–101 (2015).https://doi.org/10.1109/ICCAD.2015.7372555

    work page doi:10.1109/iccad.2015.7372555 2015

  2. [2]

    In: Piskac, R., Rakamaric, Z

    Azzopardi, S., Stefano, L.D., Piterman, N., Schneider, G.: Full LTL synthesis over infinite-state arenas. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part IV. Lecture Notes in Computer Science, vol. 15934, pp. 274–297. Springer (2025).https://do...

    work page doi:10.1007/978-3-031-98685-7_13 2025

  3. [3]

    Biere, A.: The AIGER And-Inverter Graph (AIG) format version 20071012. Tech. Rep. 07/1, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2007)

    2007

  4. [4]

    In: Heule, M., Iser, M., Järvisalo, M., Suda, M

    Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024. In: Heule, M., Iser, M., Järvisalo, M., Suda, M. (eds.) Proc. of SAT Competition 2024 – Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Report Series B, vol. B-2024-1, pp. 8–10....

    2024

  5. [5]

    Comput- ers, IEEE Transactions on100(8), 677–691 (1986)

    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. Comput- ers, IEEE Transactions on100(8), 677–691 (1986)

    1986

  6. [6]

    CoRRabs/2011.13041(2020),https://arxiv.org/abs/2011.13041

    Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of muller condi- tions. CoRRabs/2011.13041(2020),https://arxiv.org/abs/2011.13041

    work page arXiv 2011

  7. [7]

    In: Finkbeiner, B., Kovács, L

    Cosler, M., Hahn, C., Omar, A., Schmitt, F.: Neurosynt: A neuro-symbolic port- folio solver for reactive synthesis. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Con- ference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2...

    work page doi:10.1007/978-3-031-57256-2_3 2024

  8. [8]

    In: Legay, A., Margaria, T

    Esparza, J., Kretínský, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic büchi automata to deterministic parity automata. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd Interna- tional Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of S...

    work page doi:10.1007/978-3-662-54577-5_25 2017

  9. [9]

    Formal Methods Syst

    Esparza, J., Kretínský, J., Sickert, S.: From LTL to deterministic automata - A safraless compositional approach. Formal Methods Syst. Des.49(3), 219–271 (2016). https://doi.org/10.1007/S10703-016-0259-2

    work page doi:10.1007/s10703-016-0259-2 2016

  10. [10]

    https://doi.org/10.1145/3417995

    Esparza, J., Kretínský, J., Sickert, S.: A unified translation of linear temporal logic to ω-automata.J.ACM67(6),33:1–33:61(2020). https://doi.org/10.1145/3417995

    work page doi:10.1145/3417995 2020

  11. [11]

    In: Proceedings of the 2023 ACM/SIGDA International Symposium on Field Programmable Gate Arrays

    Fan, L., Wu, C.: Fpga technology mapping with adaptive gate decomposition. In: Proceedings of the 2023 ACM/SIGDA International Symposium on Field Programmable Gate Arrays. pp. 135–140 (2023)

    2023

  12. [12]

    In: Kobayashi, N., Worrell, J

    Hausmann, D., Lehaut, M., Piterman, N.: Symbolic solution of emerson-lei games for reactive synthesis. In: Kobayashi, N., Worrell, J. (eds.) Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City...

    work page doi:10.1007/978-3-031-57228-9_4 2024

  13. [13]

    Journal of the Franklin Institute257(3), 161–190 (1954)

    Huffman, D.: The synthesis of sequential switching circuits. Journal of the Franklin Institute257(3), 161–190 (1954). https://doi.org/https: //doi.org/10.1016/0016-0032(54)90574-8, https://www.sciencedirect.com/ science/article/pii/0016003254905748

    work page doi:10.1016/0016-0032(54)90574-8 1954

  14. [14]

    In: Piskac, R., Dimitrova, R

    Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Piskac, R., Dimitrova, R. (eds.) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016. EPTCS, vol. 229, pp. 112– 132 (2016).https://doi.org/10.4204/EPTCS.229.10 12

    work page doi:10.4204/eptcs.229.10 2016

  15. [15]

    arXiV (Jun 2022)

    Jacobs, S., Pérez, G.A., Abraham, R., Bruyère, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, 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.: The rea...

    work page doi:10.48550/arxiv.2206.00251 2018

  16. [16]

    International journal on software tools for technology transfer26(5), 551–567 (2024)

    Jacobs, S., Pérez, G.A., Abraham, R., Bruyere, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., et al.: The reactive synthesis competition (syntcomp): 2018–2021. International journal on software tools for technology transfer26(5), 551–567 (2024)

    2018

  17. [17]

    Volume 4a

    Knuth, D.: The Art of Computer Programming: Combinatorial algorithms, part 1. Volume 4a. Addison-Wesley (2011), https://books.google.de/books? id=jT-30QEACAAJ

    2011

  18. [18]

    In: Chen, Y., Cheng, C., Esparza, J

    Kretínský, J., Manta, A., Meggendorfer, T.: Semantic labelling and learning for parity game solving in LTL synthesis. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th Interna- tional Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp...

    work page doi:10.1007/978-3-030-31784-3_24 2019

  19. [19]

    In: Gurfinkel, A., Heule, M

    Kretínský, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: Semml: Enhancing automata-theoretic LTL synthesis with machine learning. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of S...

    2025

  20. [20]

    In: Lahiri, S.K., Wang, C

    Kretínský, J., Meggendorfer, T., Sickert, S.: Owl: A library forω-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 543–550. Springer (2018).https:...

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

  21. [21]

    Meyer and Salomon Sickert , title =

    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 doi:10.1007/s00236-019-00349-3 2020

  22. [22]

    In: Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing

    Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper, 1989). In: Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing. p. 377–410. PODC ’90, Association for Computing Machinery, New York, NY, USA (1990).https://doi.org/10.1145/93385.93442

    work page doi:10.1145/93385.93442 1989

  23. [23]

    A Mathematical Theory of Communication,

    Mealy, G.H.: A method for synthesizing sequential circuits. The Bell System Tech- nical Journal34(5), 1045–1079 (1955).https://doi.org/10.1002/j.1538-7305. 1955.tb03788.x

    work page doi:10.1002/j.1538-7305 1955

  24. [24]

    https://github.com/ incaseoftrouble/jbdd(2017)

    Meggendorfer, T.: JBDD: A java BDD library. https://github.com/ incaseoftrouble/jbdd(2017)

    2017

  25. [25]

    Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. ...

    work page doi:10.1007/978-3-319-96145-3_31 2018

  26. [26]

    Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: International Conference on Computer Aided Verification. pp. 578–586. Springer (2018)

    2018

  27. [27]

    In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings

    Piterman, N.: From nondeterministic buchi and streett automata to deterministic parity automata. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings. pp. 255–264. IEEE Computer Society (2006).https://doi.org/10.1109/LICS.2006.28

    work page doi:10.1109/lics.2006.28 2006

  28. [28]

    18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977 , pages =

    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 Octo- ber - 1 November 1977. pp. 46–57. IEEE Computer Society (1977). https: //doi.org/10.1109/SFCS.1977.32

    work page doi:10.1109/sfcs.1977.32 1977

  29. [29]

    In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D

    Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings. Lecture Notes in Computer Science, vol. 372, pp. 652–671. Springer (1989).https://doi.org/10.1...

    work page doi:10.1007/bfb0035790 1989

  30. [30]

    Formal Methods in System Design61(2), 248–289 (2022)

    Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Dissecting ltlsynt. Formal Methods in System Design61(2), 248–289 (2022)

    2022

  31. [31]

    In: Mousavi, M.R., Philippou, A

    Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Effective reduc- tions of mealy machines. In: Mousavi, M.R., Philippou, A. (eds.) Formal Techniques for Distributed Objects, Components, and Systems 42nd IFIP WG 6.1 Interna- tional Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computin...

    work page doi:10.1007/978-3-031-08679-3_8 2022

  32. [32]

    In: Proc

    Rodríguez, A., Gorostiaga, F., Sánchez, C.: Counter example guided reactive synthesis for LTL modulo theories*. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part IV. Lecture Notes in Computer Science, vol. 15934, pp. 224–248. Springer (2025).http...

    work page doi:10.1007/978-3-031-98685-7_11 2025

  33. [33]

    In: Enea, C., Lal, A

    Rodríguez, A., Sánchez, C.: Boolean abstractions for realizability modulo theories. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 305–328. Springer Nature Switzerland, Cham (2023)

    2023

  34. [34]

    In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October

    Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October

  35. [35]

    pp. 319–327. IEEE Computer Society (1988).https://doi.org/10.1109/ SFCS.1988.21948

    work page arXiv 1988

  36. [36]

    In: de Alfaro, L

    Schewe, S.: Tighter bounds for the determinisation of büchi automata. In: de Alfaro, L. (ed.) Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Lecture Notes in Co...

    work page doi:10.1007/978-3-642-00596-1_13 2009

  37. [37]

    In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

    Sickert, S., Esparza, J.: An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. p. 831–844. LICS ’20, Association for Computing Machinery, New York, NY, USA (2020).https://doi. org/10.1145/3373718.3394743 14

    work page doi:10.1145/3373718.3394743 2020

  38. [38]

    In: 1st Symposium in Logic in Computer Science (LICS)

    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program ver- ification. In: 1st Symposium in Logic in Computer Science (LICS). IEEE Computer Society (1986) 15 A LTL, Semantic Translation, and Semantic Labelling A.1 LTL Linear temporal logic (LTL) is a logic over discrete time introduced in [28]. Given a set ofatomic propositions (AP),...

    1986

  39. [39]

    simple-to-translate

    Normalize the LTL formula using the Normalization procedure of [36]. The result is a boolean combination of “simple-to-translate” subformulae

  40. [40]

    The result is an Emerson Lei automaton

    Translate each individual subformula using the simple translations presented in [10]. The result is an Emerson Lei automaton. 16

  41. [41]

    Translate the Emerson Lei automaton into a Parity automaton using the Zielonka tree construction [6]. Here we use so-calledconditionalZielonka trees, which are an unpublished optimization implemented inOwland were used already in the previous version of our tool, as well as its predecessor Strix. We proceed to talk about each of these steps in more detail...

  42. [42]

    after function

    the authors finally prove this constructively, i.e. they show how to convert any arbitrary LTL formula into such a boolean combination of Büchi formulae. This normalization procedure marks the first step in our automaton construction. Simple Translations for Fragments.In [10] the authors show how to eas- ily convert Büchi formulae to Deterministic Büchi a...

  43. [43]

    minimize the machine and use semantic encoding

  44. [44]

    minimize the machine and use binary encoding

  45. [45]

    donotminimize the machine and use semantic encoding 25

  46. [46]

    direct strategy

    donotminimize the machine and use binary encoding The reasoning is that as already noted byStrix[21], the minimization can sometimes destroy the structure that the semantic encoding is trying to capture. Thus, we also attempt the semantic encoding on the non minimized machine and the binary (smaller but unstructured) encoding on the minimized machine. The...