Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915452885663744 |
|---|---|
| author | Hausmann, Daniel Zhu, Shufang Parretti, Gianmarco Weinhuber, Christoph De Giacomo, Giuseppe Piterman, Nir |
| author_facet | Hausmann, Daniel Zhu, Shufang Parretti, Gianmarco Weinhuber, Christoph De Giacomo, Giuseppe Piterman, Nir |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_14725 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis Hausmann, Daniel Zhu, Shufang Parretti, Gianmarco Weinhuber, Christoph De Giacomo, Giuseppe Piterman, Nir Logic in Computer Science Artificial Intelligence Formal Languages and Automata Theory 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. |
| title | Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis |
| topic | Logic in Computer Science Artificial Intelligence Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2508.14725 |