О выразительных возможностях некоторых расширений линейной темпоральной логики

Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Мы полагаем, что для формального описания поведения реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционная темпоральная логика линейного времени $LTL$. В этой работе рассматривается новый язык формальных спецификаций $\mathcal{LP}$-$LTL$, представляющий собой расширение темпоральной логики $LTL$, специально разработанное для описания свойств вычислений автоматов-преобразователей. Темпоральные операторы в формулах $\mathcal{LP}$-$LTL$ снабжены параметрами, в качестве которых используются множества слов (языки), описывающие потоки сигналов управления, поступающих на вход реагирующей системы. Базовые предикаты в формулах $\mathcal{LP}$-$LTL$ также определяются языками в алфавите элементарных действий; эти языки описывают ожидаемую реакцию системы в ответ на воздействия окружающей среды. В более ранних работах авторов этой статьи изучалась задача верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами логик $\mathcal{LP}$-$LTL$ и $\mathcal{LP}$-$CTL$. Было показано, что для обеих логик эта задача алгоритмически разрешима. Цель данной работы — оценить выразительные возможности логики $\mathcal{LP}$-$LTL$ и сравнить ее с широко известными логиками, применяющимися в информатике для спецификации реагирующих систем. В логике $\mathcal{LP}$-$LTL$ были выделены два фрагмента $\mathcal{LP}$-$1$-$LTL$ и $\mathcal{LP}$-$n$-$LTL$. Нам удалось установить, что язык спецификаций $\mathcal{LP}$-$1$-$LTL$ более выразителен, чем $LTL$, в то время как фрагмент $\mathcal{LP}$-$n$-$LTL$ обладает точно такими же выразительными возможностями, что и монадическая логика второго порядка S$1$S.