Bài báo này trình bày bộ giải tổng hợp phản ứng đầu tiên cho logic thời gian LTLfp và PPLTLp, đạt được khả năng biểu đạt LTL đầy đủ trong môi trường dấu vết vô hạn bằng cách tận dụng các kỹ thuật LTLf/PPLTL dấu vết hữu hạn. Nó dựa trên một trò chơi đồ thị xây dựng đấu trường trò chơi bằng kỹ thuật LTLf/PPLTL dựa trên DFA. Đầu tiên, chúng tôi trình bày một bộ giải ký hiệu dựa trên trò chơi Emerson-Lei, rút gọn các thuộc tính cấp thấp (bảo đảm và an toàn) thành các thuộc tính cấp cao (đệ quy và tính bền vững) và giải trò chơi. Cuối cùng, chúng tôi giới thiệu trò chơi Manna-Pnueli, tích hợp tự nhiên mục tiêu Manna-Pnueli vào đấu trường. Trò chơi Manna-Pnueli được giải bằng cách tổng hợp nghiệm của DAG của trò chơi Emerson-Lei đơn giản hơn, một phương pháp hiệu quả hơn có thể chứng minh được. Chúng tôi đánh giá thử nghiệm trình giải được triển khai cho nhiều công thức khác nhau, cho thấy trò chơi Manna-Pnueli thường mang lại lợi ích đáng kể nhưng không mang tính phổ biến, cho thấy việc kết hợp hai phương pháp này có thể cải thiện hiệu suất thực tế hơn nữa.
