A Compositional Framework for On-the-Fly LTLf Synthesis

## КОНТЕКСТ И ПРОБЛЕМАТИКА Реактивная синтезирование систем из логики линейного временного порядка на конечных трассах (LTLf) является важной задачей в области автоматического проектирования реактивных систем. Оно заключается в построении контроллера, который гарантирует выполнение заданной спецификации, заданной в виде LTLf-формулы. Традиционно, это сводится к решению двухуровневой игры над Детерминированным Конечным Автоматом (DFA), построенным из LTLf-спецификации. Однако, построение такого DFA представляет сложную вычислительную задачу, которая является 2EXPTIME-complete в худшем случае. Существующие подходы к решению этой проблемы можно разделить на два ключевых направления. Первый подход заключается в композиционном построении DFA до решения игры, что позволяет использовать минимизацию автомата для снижения сложности вычислений. Однако, этот подход может быть неэффективен при работе с большими спецификациями, которые требуют полного построения автомата. Второй подход — инкрементальное построение DFA в процессе решения игры, что позволяет избежать полного построения автомата, но может привести к неоптимальным решениям из-за отсутствия полной информации о структуре системы. В данной работе авторы предлагают новый композиционный подход, который интегрирует преимущества обоих методов. Он ориентирован на решение задач, где спецификация представляет собой большую конъюнкцию меньших LTLf-формул, что является типичным случаем в практических приложениях. Цель состоит в том, чтобы создать более эффективный фреймворк для синтеза, который мог бы обрабатывать большие и сложные спецификации, избегая неэффективности существующих методов. ## ПРЕДЛОЖЕННЫЙ МЕТОД Предлагаемый метод основывается на композиционном подходе к синтезу LTLf, который интегрирует процесс композиции с решением игры, а не с построением DFA. Это достигается за счет разбиения спецификации на меньшие компоненты, которые затем компонуются в процессе решения игры. Авторы предлагают два варианта композиции: первый вариант включает в себя предварительную минимизацию и последующую композицию, в то время как второй вариант основывается на инкрементальной композиции в процессе синтеза. Ключевой инновацией является то, что композиция выполняется «на лету», в процессе решения игры, а не заранее. Это позволяет избежать полного построения DFA, тем самым снижая сложность вычислений. Кроме того, предлагается механизм упрощения (pruning) промежуточных результатов, который позволяет уменьшить сложность последующих композиций и обнаруживать невыполнимость спецификации раньше. ## ЭКСПЕРИМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ Для оценки эффективности предлагаемого метода авторы провели серию экспериментов на различных наборах данных. Эти данные включали в себя большие и сложные LTLf-спецификации, которые характеризовались высокой степенью композиционности. Эксперименты показали, что предлагаемый метод способен решать значительно больше задач, чем существующие методы. В частности, было показано, что оба варианта композиции — предварительная минимизация и инкрементальная композиция — имеют свои преимущества. Предварительная минимизация позволяет достичь большей эффективности в случаях, когда спецификация может быть значительно упрощена, в то время как инкрементальная композиция лучше подходит для динамического управления процессом синтеза. ## ПРАКТИЧЕСКАЯ ЗНАЧИМОСТЬ Предлагаемый фреймворк имеет широкое применение в области автоматического проектирования реактивных систем, особенно в тех случаях, когда спецификации являются крупными и состоят из множества меньших компонентов. Этот подход может быть использован в различных приложениях, таких как автоматизация производственных процессов, разработка автономных систем и проектирование программного обеспечения с высокими требованиями к надежности. Преимущества этого метода заключаются в его способности обрабатывать большие и сложные спецификации, а также в его гибкости, которая позволяет выбирать между различными стратегиями композиции в зависимости от конкретной задачи. ## ВЫВОДЫ И ПЕРСПЕКТИВЫ В работе был представлен новый композиционный фреймворк для синтеза LTLf, который интегрирует композицию и решение игры в единый процесс. Этот подход демонстрирует высокую эффективность и способность решать задачи, недоступные для существующих методов. Будущие исследования могут быть направлены на дальнейшее улучшение эффективности метода, в том числе путем разработки более продвинутых методов минимизации и оптимизации процесса композиции. Кроме того, можно изучить возможности применения этого фреймворка к другим типам спецификаций и задач синтеза.