Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis

## Контекст Логические языки для реактивного синтеза, такие как LTLf (Linear Temporal Logic for Finite Traces) и PPLTL (Positive Past Linear Temporal Logic), обладают высоким потенциалом для моделирования и анализа систем, работающих в реальном времени. Однако их приложения ограничиваются моделированием систем с бесконечными трассами. Расширение логики LTLf/PPLTL для работы с бесконечными трассами, сохраняя их выразительность, лежит в основе нового подхода, основанного на ранее введенной Manna-Pnueli Hierarchy. Несмотря на этот прогресс, реализации синтеза, основанные на этой теории, отсутствовали до текущего исследования. ## Метод Для получения решений в LTLf+ и PPLTL+ используется метод Emerson-Lei и Manna-Pnueli, основанных на играх на графах. Emerson-Lei games строятся с использованием DFA (Deterministic Finite Automaton) из LTLf/PPLTL, чтобы сократить проблемы со скоростью выполнения. Manna-Pnueli games, в свою очередь, являются продолжением идеи Emerson-Lei, но они ориентированы на более эффективное решение, поскольку они логически включают Manna-Pnueli-объектив в игровую арену. Для решения используется подход, основанный на составном решении DAG (Directed Acyclic Graph) Emerson-Lei, что дает более эффективную алгоритмическую реализацию. ## Результаты Используя данные из различных практических случаев, были проведены эксперименты с полученными решениями. Результаты показали, что Manna-Pnueli games часто демонстрируют выигрыш в производительности по сравнению с Emerson-Lei games. Тем не менее, не всегда это преимущество является универсальным. Таким образом, улучшенный подход может включать комбинирование обеих методологий, чтобы улучшить практическое применение. ## Значимость Результаты этих исследований открывают путь к расширению возможностей LTLf/PPLTL в более широких областях синтеза. Это может иметь значительное влияние на разработку систем, основанных на логике бесконечных трасс, таких как автоматическое управление и системы мониторинга в реальном времени. Будущие исследования могут сосредоточиться на совершенствовании комбинированного подхода и его применении в реальных системах. ## Выводы Представленный подход представляет собой прорыв в реактивном синтезе для LTLf+ и PPLTL+. Он позволяет эффективно использовать концепции Manna-Pnueli в рамках DFA-объективов LTLf/PPLTL, повышая производительность. Несмотря на то, что Emerson-Lei games могут быть достаточно эффективными в некоторых случаях, комбинирование обеих методологий может привести к еще более устойчивым решениям в будущем.