This paper presents the first reactive synthesis solver for temporal logic LTLfp and PPLTLp, which achieves full LTL expressivity in an infinite-trace environment by leveraging finite-trace LTLf/PPLTL techniques. It is based on a graph game that constructs a game arena using a DFA-based LTLf/PPLTL technique. First, we present a symbolic solver based on the Emerson-Lei game, which reduces low-level properties (guarantees and safety) to high-level properties (recursivity and persistence) and solves the game. Finally, we introduce the Manna-Pnueli game, which naturally incorporates the Manna-Pnueli objective into the arena. The Manna-Pnueli game is solved by synthesizing the solution to the DAG of the simpler Emerson-Lei game, a provably more efficient approach. We experimentally evaluate the implemented solver for various formulations, showing that the Manna-Pnueli game often offers significant benefits, but is not universal, suggesting that combining the two approaches could further improve practical performance.
