Este artículo presenta el primer solucionador de síntesis reactiva para lógica temporal LTLfp y PPLTLp, que logra plena expresividad LTL en un entorno de trazas infinitas mediante técnicas LTLf/PPLTL de trazas finitas. Se basa en un juego gráfico que construye una arena de juego mediante una técnica LTLf/PPLTL basada en DFA. En primer lugar, presentamos un solucionador simbólico basado en el juego de Emerson-Lei, que reduce las propiedades de bajo nivel (garantías y seguridad) a propiedades de alto nivel (recursividad y persistencia) y resuelve el juego. Finalmente, presentamos el juego Manna-Pnueli, que incorpora de forma natural el objetivo de Manna-Pnueli en la arena. El juego Manna-Pnueli se resuelve sintetizando la solución al DAG del juego más simple de Emerson-Lei, un enfoque demostrablemente más eficiente. Evaluamos experimentalmente el solucionador implementado para varias formulaciones, mostrando que el juego Manna-Pnueli a menudo ofrece beneficios significativos, pero no es universal, lo que sugiere que combinar los dos enfoques podría mejorar aún más el rendimiento práctico.
