Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis

Christoph Weinhuber; Daniel Hausmann; Gianmarco Parretti; Giuseppe De Giacomo; Nir Piterman; Shufang Zhu

REVIEW 2 major objections 6 minor 4 references

Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis

T0 review · 2 major / 6 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read To solve reactive synthesis for LTLf+ and PPLTL+, the paper introduces Manna-Pnueli games, which mix guarantee, safety, recurrence, and persistence objectives, and proves they can be solved by composing solutions to a DAG of simpler Emerson

desk verdict Useful paper with a real, fixable gap in the central algorithmic claim: the bottom-up DAG composition in Section 6 is asserted but not proved, and the stress-test counterexample shows it is not sound as literally stated. read the letter →

arxiv 2508.14725 v1 pith:LCITPT4P submitted 2025-08-20 cs.LO cs.AIcs.FL

Daniel Hausmann , Shufang Zhu , Gianmarco Parretti , Christoph Weinhuber , Giuseppe De Giacomo , Nir Piterman This is my paper

classification cs.LOcs.AIcs.FL MSC 68Q6091A5068Q45

keywords reactivesynthesisLTLf+PPLTL+Manna-PnueligamesEmerson-Leifinite-tracetemporallogicsymbolicgamesolvingDAGof

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

The paper aims to build real solvers for reactive synthesis in LTLf+ and PPLTL+, two logics that describe infinite behavior by combining finite-trace properties from the Manna-Pnueli hierarchy: guarantee, safety, recurrence, and persistence. It introduces Manna-Pnueli games, which keep those four condition types separate instead of reducing every condition to the recurrence/persistence form used in Emerson-Lei games. The paper proves that solving a Manna-Pnueli game through a directed acyclic graph of simpler Emerson-Lei games is asymptotically faster than the naive reduction, and it reports an implemented synthesizer where the MP approach often outperforms the EL approach on tested formulas. If correct, this gives the first implemented synthesis tools for these logics and makes expressive full-LTL-class specifications more practical.

What carries the argument

The central object is a Manna-Pnueli game: an infinite-duration game with an objective built as a positive Boolean combination of four temporal event conditions—F a (eventually a), G a (always a), GF a (a infinitely often), and FG a (a cofinally). The core mechanism is an arena transformation that annotates nodes with memory L recording which F-events have occurred and which G-events have been violated; the memory update is monotone, so memory values change only finitely often. This partitions the arena into subarenas with fixed memory, arranged as a directed acyclic graph. Each subgame's objective simplifies to a purely Emerson-Lei formula φ_L, so the whole game is solved bottom-up by solvi

What would settle it

Take a small Manna-Pnueli game with two local events, solve it both by the DAG-composition procedure and by directly solving the equivalent Emerson-Lei game G2 with the paper's symbolic fixpoint method, and compare the winning regions; any mismatch at a node would refute the composition.

Watch

Extended reading notes

Core claim

The central claim is that Manna-Pnueli games—objectives that are positive Boolean combinations of F, G, GF, and FG event conditions—can be solved by composing solutions to a DAG of simpler Emerson-Lei games, and that this composition is provably more efficient than translating all conditions into Emerson-Lei events. Concretely, an MP game with n nodes, k Emerson-Lei events, and d local events is solvable in time O(k! * n^(k+2) * 2^d) with strategies of size k! * 2^d (Theorem 4), while the naive EL reduction costs O((k+d)! * (n*2^d)^(k+d+2)) (Corollary 1). Because LTLf+ and PPLTL+ formulas translate directly into deterministic MP automata—one DFA per finite-trace component, with local-event m

Load-bearing premise

The argument depends on an asserted step: that solving each subgame of the directed acyclic graph separately, and marking incoming edges as winning or losing from the subgame result, computes the full winning region of the combined game.

Editorial extensions

If this is right

LTLf+ and PPLTL+ synthesis become practically solvable: the paper's implementation is the first for these logics, and the MP-based solver often beats the EL-based one on the tested formulas.
Manna-Pnueli games whose arenas already carry local-event memory are solved in time O(m * k! * n^k) with strategies of k! memory states—the same asymptotic cost as pure Emerson-Lei games.
Guarantee and safety conditions no longer need to be translated into recurrence/persistence before solving; treating them as local events removes their contribution to the factorial factor in the complexity.
For obligation properties built only from guarantee and safety, MP games reduce to DAGs of reachability and safety games, solvable in O(2^d * m) time with at most 2^d memory states.
The two approaches trade off in practice: on formulas with many pure guarantee conditions the EL solver can be faster because its automata construction short-circuits nested fixpoints, so hybrid strategies are the likely next practical improvement.

Reading between the lines

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

The same memory-based DAG decomposition should transfer to other prefix-dependent objectives: any objective whose truth can be tracked by a monotone finite memory induces a DAG of subgames with simplified objectives.
The complexity gap predicts MP's advantage should widen as the number of local events grows with the number of Emerson-Lei events fixed; a benchmark sweep varying only d would test this directly.
A dedicated engine for the obligation fragment could plausibly approach reachability-game performance, since every subgame in that fragment is a reachability or safety game.
The correctness of the bottom-up DAG composition, asserted from the DAG structure rather than proven by a dedicated lemma, is the natural target for a formal proof or a small counterexample search.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Things you should know before sending a referee at this: the paper introduces Manna-Pnueli (MP) games and gives the first LTLf+/PPLTL+ synthesis solvers. That part is real. The automata constructions in Sections 3 and 5 are careful and correct under standard conventions (one minor missing convention about empty traces). The EL reduction and the MP game notion are new, and the complexity comparison between Theorem 4 and Corollary 1 is accurately drawn. The experiments honestly show MP doesn't always beat EL; they don't overclaim.

The soft spot is the proof of Theorem 4. The paper claims G2 can be solved bottom-up by solving each subgame GL with its own objective φL and marking incoming edges as winning/losing. Lemma 5 only proves G and G2 equivalent; it doesn't prove this compositional procedure computes G2's winning region. And as stated, the procedure fails on a simple example: a single system node labeled with {a}, objective F a. The subgame G∅ has objective ⊥ and the only edge goes to the previously solved winning subgame G{a}; solving G∅ literally as a game with objective ⊥ declares the whole game losing, which is wrong. To make it work, each GL needs to be solved as a game with an objective that includes reachability to already-determined winning terminals and avoidance of losing ones, or something equivalent; that modification isn't stated or proved. So the O(2^d·m·k!·n^k) bound rests on an unproved, as-written incorrect compositional step.

This is fixable. The DAG decomposition idea is sound; the missing piece is a standard textbook treatment of games on DAGs. But it's not a cosmetic omission. A referee should insist on a lemma that states and proves the correctness of the bottom-up algorithm, including the treatment of exit edges. The empty-trace convention for the DFA constructions should also be stated.

Overall: the paper deserves a serious referee. It's a solid contribution to the reactive synthesis literature if the gap is closed. My recommendation is to send it out, with a specific request that the reviewer examine Section 6 closely. If the authors supply the missing proof, this should be accepted. If they can't, Theorem 4 falls back to Corollary 1 and the MP solver loses its main theoretical justification.

Referee Report

2 major / 6 minor

Summary. The paper presents the first implemented solvers for synthesis in LTLf+ and PPLTL+ by reducing formulas to infinite-duration games. It first gives an Emerson-Lei (EL) game construction (Section 3), then introduces Manna-Pnueli (MP) games whose objectives natively combine guarantee, safety, recurrence, and persistence atoms (Section 4). Section 5 shows that LTLf+/PPLTL+ formulas translate directly to MP games. Section 6 claims that an MP game can be solved by building a DAG of EL subgames and solving them bottom-up, yielding the improved bound O(k! n^{k+2} 2^d) over the naive reduction to one EL game with k+d events. The authors implement both solvers in LydiaSyft+ and report experiments on planning-inspired benchmarks. The central theoretical and practical claims depend on the soundness of the compositional DAG solver in Section 6.

Significance. If the main result holds, the paper makes a useful contribution: MP games are a natural intermediate formalism between LTLf+/PPLTL+ specifications and EL/parity games, and the claimed separation between a 2^d factor for local events and a k! factor for EL events is theoretically interesting. The paper also ships a concrete implementation and an experimental comparison, which is valuable for a synthesis venue. However, the key algorithmic step—solving an MP game by composing solutions of EL subgames—is asserted rather than proved, and as literally stated it is incorrect on a minimal example. The theoretical complexity theorem and the solver's claimed advantages therefore rest on an unsupported and, as written, false algorithmic claim. The contribution is significant enough to merit a major revision if the authors can supply a correct composition lemma and adapt the proof (and, if needed, the algorithm).

major comments (2)

[Section 6, paragraph beginning "Due to its particular DAG structure..."] Falls under major comment 1.
[Section 6, Remark 5 and Theorem 4 (strategy-size bound)] Falls under major comment 1.

minor comments (6)

[Section 5, paragraph after Theorem 3] “The alternative synthesis algorithm given in Section 5 leverages this improved reduction” should refer to Section 6, not Section 5.
[Section 5, complexity paragraph] “guarantuee” is a typo for “guarantee”.
[Section 6, definition of φ2] The formula φ2 = W_{L∈2^{ΓF,G}} (V_{a∈L} Inf a ∧ φL) uses “W” and “V” without explaining the notation, and “Inf a” is never defined. Use ∨/∧ and define Inf a = GF a.
[Supplement, full proof of Lemma 5 (second direction)] The sentence “By Lemma 4, π′ |= φ which implies π |= φ” is not the lemma’s statement applied correctly; it should presumably read “π |= φL implies π |= φ” (or similar). Please correct the typo.
[Section 4, after definition of MP games] “By definition, MP games are determined” is imprecise: determinacy of perfect-information games with Borel objectives is a theorem, not part of the definition. Please cite determinacy or say “MP games are determined by known results.”
[Example 1 and Figure 2] The text describing the example graph (“dc, d a, d b, a c G”) is garbled and the figure is hard to read. Please redraw/relabel so the example is self-contained.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the MP-game solver is a genuinely new compositional construction; its reliance on independently published EL-game results and the Aminof et al. reduction is external support, not a self-referential loop.

full rationale

The paper's derivation chain does not reduce to its own inputs. Theorem 4's complexity bound is obtained by combining Theorem 1 (EL games solvable in O(k! n^{k+2})), which is cited to McNaughton/Zielonka and to Hausmann, Lehaut & Piterman 2024. Although the latter has overlapping authorship, it is an independently published, proof-carrying result, not a claim manufactured for this paper; Rule 3 treats such citations as genuine evidence. The reduction from LTLf+/PPLTL+ formulas to EL automata is explicitly credited to Aminof et al. 2025b (Proposition 1), and the MP-automaton translation (Proposition 2) is proved from DFAs for the finite-trace components; it is a direct semantic translation, not a renaming of the target result. The claimed asymptotic advantage of Manna-Pnueli games over the naive EL reduction (Corollary 1 vs Theorem 4) is arithmetic comparison of two stated bounds. The only in-scope concern is Section 6's assertion "Due to its particular DAG structure, the game G2 can be solved by solving the subgames GL ... individually..." : this bottom-up marking procedure is asserted without a formal soundness proof, so a literal reading can misclassify games where plays exit a subgame before the local memory stabilizes. That is a genuine correctness/omitted-proof risk, which the reviewer should weigh elsewhere, but it is not circularity: the algorithm is not assumed as an input, no equation is defined in terms of its conclusion, and no fitted parameter is relabelled as a prediction. Accordingly no circular step is identified.

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

The paper's central results rest on established EL game solving (Theorem 1), cited DFA translation bounds, the prior EL-reduction of LTLf+/PPLTL+ (Aminof et al. 2025b), and two items specific to this paper: the asserted soundness of the bottom-up DAG composition, and an unstated convention about the empty finite trace. There are no fitted constants anywhere; the ledger contains no free parameters.

assumptions (5)

standard math EL games with n nodes and k events are solvable in O(k!*n^(k+2)) with k! memory strategies (Theorem 1).
Invoked as the black-box solver for every subgame in Section 6; taken from McNaughton 1993, Zielonka 1998, and Hausmann, Lehaut, Piterman 2024.
standard math LTLf formulas translate to DFAs of size at most doubly exponential in the formula, PPLTL to at most exponential, via cited constructions.
Section 2 and Steps 1/1a rely on these bounds for the 2EXPTIME/EXPTIME claims and for the arena sizes n' = 2^(2^n) resp. 2^n.
domain assumption The LTLf+/PPLTL+ to EL-automaton reduction of Aminof et al. 2025b is correct (Proposition 1).
Cited, not re-proven; the EL solver in Section 3 stands or falls on it.
ad hoc to paper Solving subgames GL bottom-up with exit edges marked by already-computed winners correctly solves G2.
Asserted in the paragraph 'Due to its particular DAG structure...' in Section 6; no lemma proves the composition algorithm equals the G2 winning condition. This is the weakest assumption.
domain assumption Fixed convention for whether the empty finite trace is a prefix and for the initial-state acceptance of the component DFAs.
Lemma 2 and the initial-state add/remove steps in Section 5 are only correct under a specific convention about epsilon in [Phi_i]; the paper does not state the convention.

invented entities (1)

Manna-Pnueli game objectives (positive Boolean combinations of F, G, GF, FG atoms with 'local' F/G events) independent evidence
purpose: Native embedding of LTLf+/PPLTL+ synthesis objectives so guarantee/safety conditions are not reduced to recurrence/persistence before solving.
A formal device, not an empirical postulate; it carries falsifiable handles through the correctness lemmas (Lemma 5), the complexity bound (Theorem 4), and the implemented solvers, any of which could be refuted by counterexample.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis." pith.science (2026). https://pith.science/paper/LCITPT4P

@misc{pith2026250814725,
  author       = {Pith},
  title        = {Pith review of: Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LCITPT4P}},
  note         = {Machine review of arXiv:2508.14725}
}

read the original abstract

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLfp and PPLTLp, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.

Figures

Figures reproduced from arXiv: 2508.14725 by the authors.

**Figure 1.** Overall structure of the implementation complexity of solving G2 in this way is in O(2d ·m·k!·n k ). Note that we have m ≤ n 2 . Theorem 4. Manna-Pnueli games with n nodes, k Emerson-Lei events and d local events can be solved in time O(k! ·n k+2 · 2 d ) ∈ 2 O(d+k log n) ; winning strategies require at most k! · 2 d memory values. The above bounds improve to a solution time O(m · k! · n k ) ∈ 2 O(k log n) and strate… view at source ↗

**Figure 2.** A simple planning domain DFA. Since all DFAs are in symbolic representation, we can avoid explicitly computing their cross-product. Instead, we perform an on-the-fly product construction during the EL game solving, which is carried out using symbolic fixpoint computations as in (Zhu et al. 2017b; Hausmann, Lehaut, and Piterman 2024). Synthesis via MP solver. We also implemented the MP based approach to LTLf+/PPLTL+ … view at source ↗

**Figure 4.** Runtime of LTLf + synthesis, (∀∃ → ∃)-Pattern [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗

Figures from the paper (1 more)

**Figure 5.** Figure 5: Runtime of LTLf + synthesis, ∃-Pattern benchmark are realizable as well [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

4 extracted references · 3 canonical work pages

[2003]

Weak, strong, and strong cyclic planning via sym- bolic model checking. Artif. Intell. 1–2(147). De Giacomo, G., and Favorito, M. 2021. Compositional approach to translate LTL f /LDLf into deterministic finite automata. In ICAPS. De Giacomo, G., and Rubin, S. 2018. Automata-theoretic foundations of fond planning for LTL f /LDLf goals. In IJ- CAI. De Giaco...

work page 2021
[2017]

Preliminaries

Supervisory control and reactive synthesis: a compar- ative introduction. Discret. Event Dyn. Syst. 27(2):209–260. Emerson, E. A., and Lei, C. 1987. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program. 8(3):275–306. Fijalkow, N.; Bertrand, N.; Bouyer-Decitre, P.; Brenguier, R.; Carayol, A.; Fearnley, J.; Gimbert, H.; Hor...

arXiv 1987
[2020]

In IJCAI

Pure-past linear temporal and dynamic logic on finite traces. In IJCAI. De Giacomo, G.; Stasio, A. D.; Tabajara, L. M.; Vardi, M. Y .; and Zhu, S. 2022. Finite-trace and generalized- reactivity specifications in temporal synthesis.Formal Meth- ods Syst. Des. 61(2):139–163. Duret-Lutz, A. 2025. Personal communication. Dziembowski, S.; Jurdzinski, M.; and W...

work page 2022
[2024]

Shielded FOND: Planning with safety constraints in pure-past linear temporal logic. In ECAI. Bryant, R. E. 1992. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3):293–318. Calvanese, D.; De Giacomo, G.; and Vardi, M. Y . 2002. Reasoning about actions and planning in LTL action theo- ries. In KR. Camacho, A.; Bien...

work page 1992

Pith tools

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

[1] [2003]

Weak, strong, and strong cyclic planning via sym- bolic model checking. Artif. Intell. 1–2(147). De Giacomo, G., and Favorito, M. 2021. Compositional approach to translate LTL f /LDLf into deterministic finite automata. In ICAPS. De Giacomo, G., and Rubin, S. 2018. Automata-theoretic foundations of fond planning for LTL f /LDLf goals. In IJ- CAI. De Giaco...

work page 2021

[2] [2017]

Preliminaries

Supervisory control and reactive synthesis: a compar- ative introduction. Discret. Event Dyn. Syst. 27(2):209–260. Emerson, E. A., and Lei, C. 1987. Modalities for model checking: Branching time logic strikes back. Sci. Comput. Program. 8(3):275–306. Fijalkow, N.; Bertrand, N.; Bouyer-Decitre, P.; Brenguier, R.; Carayol, A.; Fearnley, J.; Gimbert, H.; Hor...

arXiv 1987

[3] [2020]

In IJCAI

Pure-past linear temporal and dynamic logic on finite traces. In IJCAI. De Giacomo, G.; Stasio, A. D.; Tabajara, L. M.; Vardi, M. Y .; and Zhu, S. 2022. Finite-trace and generalized- reactivity specifications in temporal synthesis.Formal Meth- ods Syst. Des. 61(2):139–163. Duret-Lutz, A. 2025. Personal communication. Dziembowski, S.; Jurdzinski, M.; and W...

work page 2022

[4] [2024]

Shielded FOND: Planning with safety constraints in pure-past linear temporal logic. In ECAI. Bryant, R. E. 1992. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3):293–318. Calvanese, D.; De Giacomo, G.; and Vardi, M. Y . 2002. Reasoning about actions and planning in LTL action theo- ries. In KR. Camacho, A.; Bien...

work page 1992