ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Bookmark

Next issue

4
Publication date:
16 September 2020
-->

Algorithmical power of some fragments of computational tree logic

Date of submission article: 2016-10-06
UDC: 510.52, 510.643
The article was published in issue no. № 4, 2016 [ pp. 135–142 ]
Abstract:In the paper we consider the Computational Tree Logic CTL and study computational complexity of the decision problem for its finitely-many variable fragments. We give a polynomial-time algorithm solving the decision problem for the variable-free fragment of CTL. We also give a polynomial-time algorithm which embeds the fragment of CTL with the modalities
Аннотация:В работе рассматривается логика ветвящегося времени CTL и изучается вопрос о сложности проблемы ее разрешения в языке с конечным числом переменных. Приведен полиномиальный алгоритм, решающий задачу принадлежности формул константному фрагменту CTL. Приведен полиномиальный алгоритм, который погружает фрагмент CTL в языке с модальностями
Authors: A.V. Dukhovneva (kugusheva_nastya@list.ru) - School of Speed Reading and Development of Intellect IQ007 (Trainer and Consultant), Tver, Russia, M.N. Rybakov (m_rybakov@mail.ru) - Tver State University, R&D Institute Centerprogramsystem (Associate Professor, Software Engineer, Research Fellow), Tver, Russia, Ph.D, D.P. Shkatov (shkatov@gmail.com) - University of the Witwatersrand (Ph.D.(Theoretical Computer Science), Senior Lecturer), Johannesburg, Ph.D
Keywords: computational complexity, decision problem, computational tree logic, temporal logic, non-classical logics, propositional logics
Page views: 2681
Print version
Full issue in PDF (16.17Mb)
Download the cover in PDF (0.62Мб)

Font size:       Font:

Для описания различных свойств сложных систем и для их последующей верификации требуются формальные языки, предполагающие четкость и однозначность формулировок. Широко используемый в математике язык логики предикатов (см., например, [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

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

 

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


Permanent link:
http://swsys.ru/index.php?page=article&id=4230&lang=en
Print version
Full issue in PDF (16.17Mb)
Download the cover in PDF (0.62Мб)
The article was published in issue no. № 4, 2016 [ pp. 135–142 ]

Perhaps, you might be interested in the following articles of similar topics: