Программные продукты и системы

Для описания различных свойств сложных систем и для их последующей верификации требуются формальные языки, предполагающие четкость и однозначность формулировок. Широко используемый в математике язык логики предикатов (см., например, [1]) во многих случаях позволяет создавать подобные описания, но в силу теоремы Чёрча–Тьюринга проблемы тождественной истинности, тождественной ложности и выполнимости формул этого языка алгоритмически неразрешимы (см., например, [2]). Это создает существенное препятствие в его использовании для решения соответствующих задач с применением вычислительной техники.

На данный момент уже созданы, изучены и используются различные классы формальных языков, логик и теорий, которые, с одной стороны, позволяют описывать свойства сложных систем, структур, вычислений и т.п., при этом, с другой стороны, многие важные проблемы для них алгоритмически разрешимы.

В данной работе речь пойдет об одном из таких языков – языке логики ветвящегося времени, которая известна в англоязычной литературе как computational tree logic и обычно обозначается CTL. Эта логика возникла относительно давно, и сейчас изучены многие ее свойства – алгоритмические, синтаксические, семантические и др.

Особенность языка CTL в том, что, во-первых, вычисления понимаются как пути, образованные состояниями, в которых последовательно оказывается система при выполнении некоторой про- граммы, а во-вторых, в языке эти состояния не указываются явно: для указания на них используются так называемые темпоральные (временны́е) модальности типа «в каждом пути когда-нибудь будет, что…», «существует путь, в котором всегда верно, что…» и т.п. Использование подобных средств позволяет описывать различные свойства программных вычислений, в том числе параллельных, что вместе с разрешимостью проблемы выполнимости CTL-формул делает CTL эффективным инструментом как для создания таких описаний, так и для верификации программ (см., например, [3, 4]).

Однако за богатые возможности приходится платить. Но если в случае классической логики предикатов имеет место неразрешимость проблемы выполнимости, то в случае CTL – только высокая степень сложности проблемы разреше- ния [5, 6]. Известно, что проблема разрешения для CTL является EXPTIME-полной. Это означает, что, во-первых, существует алгоритм, решающий проблему выполнимости CTL-формул за экспоненциальное время от длины тестируемой формулы [7], а во-вторых, любой детерминированный алгоритм, решающий эту проблему, для некоторых формул будет затрачивать время, ограниченное снизу экспонентой от длины этих формул [8]. Другими словами, в классе детерминированных алгоритмов самыми быстрыми решающими проблему выполнимости CTL-формул являются экспоненциальные, и понизить эту оценку, например, до полиномиальной, невозможно.

Нечто похожее справедливо для всех логик, содержащих в себе классическую логику высказываний CL (classical logic): проблема выполнимости CL-формул является NP-полной, и в пред­положении, что P ≠ NP, она тоже не решается быстрее, чем экспоненциально. Поскольку, как правило, известные логики содержат в себе CL в качестве естественного фрагмента, проблема их разрешения не может быть ниже.

Тем не менее CL содержит довольно выразительные фрагменты, которые полиномиально разрешимы. Например, полиномиально разрешима проблема выполнимости CL-формул, находящихся в совершенной дизъюнктивной или совершенной конъюнктивной нормальной форме (СДНФ, СКНФ): для выполнимости формулы в СДНФ достаточно, чтобы она содержала хотя бы один дизъюнктивный член, а для выполнимости формулы в СКНФ достаточно, чтобы число попарно различных конъюнктивных членов в ней было меньше чем 2n, где n – число переменных, входящих в эту формулу.

Другой пример – это любой фрагмент CL, состоящий из формул, построенных из переменных, входящих в некоторое фиксированное конечное множество. Действительно, если имеется всего одна переменная, то достаточно проверять истинность формул на двух наборах истинностных значений для нее, если имеются две переменные – на четырех наборах, если три – на восьми наборах и т.д. При этом каждый раз число таких наборов будет фиксированным, следовательно, проблема выполнимости формул из соответствующего фрагмента требует для ее решения лишь полиномиальных (не более чем квадратичных) затрат времени.

Пусть L – некоторая логика, n – неотрицательное целое число. Через L(n) обозначим фрагмент логики L, состоящий из формул от фиксированных n переменных. В частности, L(0) – константный фрагмент L. Тогда, согласно сказанному выше, для всякого целого неотрицательного n фрагмент CL(n) полиномиально разрешим. Можно ли утверждать то же самое о CTL(n)? Ответу на этот вопрос, а также его обоснованию и посвящена данная работа.

Ниже будет показано, что фрагмент CTL(0) действительно полиномиально разрешим, и будет приведен соответствующий разрешающий алгоритм. Что касается фрагментов CTL(n) при n > 0, то здесь ситуация иная. Для некоторых модальных логик доказано, что проблема разрешения их фрагментов от конечного числа переменных является столь же сложной, как и проблема разрешения для логики в целом [9–13]; аналогичные результаты справедливы и для некоторых других неклассических логик [14, 15]. Покажем, что техника, изложенная в [13, 16], применима к CTL, доказав с ее помощью, что при любом n > 0 фрагмент CTL(n) является EXPTIME-полным.

Синтаксис и семантика CTL

Будем считать, что формулы строятся из констант ⊥ (ложь) и ⊤ (истина), а также счетного множества пропозициональных переменных с помощью связок ∧ (конъюнкция), ∨ (дизъюнкция), → (импликация), ¬ (отрицание), ↔ (эквивалентность) и модальностей ????? При этом первые шесть модальностей являются одноместными и позволяют из формулы ? получать формулы , а последние две являются двухместными и позволяют из формул ? и ? получать формулы???? Каждая из этих модальностей состоит из двух частей: первая – это

Подробнее см.