Cet article présente le premier solveur de synthèse réactive pour la logique temporelle LTLfp et PPLTLp. Il atteint une expressivité LTL complète dans un environnement à traces infinies grâce aux techniques LTLf/PPLTL à traces finies. Il repose sur un jeu de graphes qui construit une arène de jeu à l'aide d'une technique LTLf/PPLTL basée sur l'AFD. Nous présentons d'abord un solveur symbolique basé sur le jeu d'Emerson-Lei, qui réduit les propriétés de bas niveau (garanties et sécurité) à des propriétés de haut niveau (récursivité et persistance) et résout le jeu. Enfin, nous introduisons le jeu de Manna-Pnueli, qui intègre naturellement l'objectif de Manna-Pnueli dans l'arène. Le jeu de Manna-Pnueli est résolu en synthétisant la solution du DAG du jeu d'Emerson-Lei plus simple, une approche manifestement plus efficace. Nous évaluons expérimentalement le solveur implémenté pour diverses formulations, montrant que le jeu Manna-Pnueli offre souvent des avantages significatifs, mais n'est pas universel, suggérant que la combinaison des deux approches pourrait encore améliorer les performances pratiques.
