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

Публикационная активность

(сведения по итогам 2017 г.)
2-летний импакт-фактор РИНЦ: 0,500
2-летний импакт-фактор РИНЦ без самоцитирования: 0,405
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,817
5-летний импакт-фактор РИНЦ: 0,319
5-летний импакт-фактор РИНЦ без самоцитирования: 0,264
Суммарное число цитирований журнала в РИНЦ: 6012
Пятилетний индекс Херфиндаля по цитирующим журналам: 404
Индекс Херфиндаля по организациям авторов: 338
Десятилетний индекс Хирша: 17
Место в общем рейтинге SCIENCE INDEX за 2017 год: 527
Место в рейтинге SCIENCE INDEX за 2017 год по тематике "Автоматика. Вычислительная техника": 16

Больше данных по публикационной активности нашего журнале за 2008-2017 гг. на сайте РИНЦ

Вход


Забыли пароль? / Регистрация

Добавить в закладки

Следующий номер на сайте

4
Ожидается:
16 Декабря 2018

Алгоритмическая выразительность некоторых фрагментов языка логики ветвящегося времени

Algorithmical power of some fragments of computational tree logic
Дата подачи статьи: 2016-10-06
УДК: 510.52, 510.643
Статья опубликована в выпуске журнала № 4 за 2016 год. [ на стр. 135–142 ][ 01.12.2016 ]
Аннотация:В работе рассматривается логика ветвящегося времени CTL и изучается вопрос о сложности проблемы ее разрешения в языке с конечным числом переменных. Приведен полиномиальный алгоритм, решающий задачу принадлежности формул константному фрагменту CTL. Приведен полиномиальный алгоритм, который погружает фрагмент CTL в языке с модальностями
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
Авторы: Духовнева А.В. (kugusheva_nastya@list.ru) - Школа скорочтения и развития интеллекта IQ007, Тверь, Россия, Рыбаков М.Н. (m_rybakov@mail.ru) - Тверской государственный университет; НИИ «Центрпрограммсистем»; Университет Витвотерсранда, Тверь, Россия, кандидат физико-математических наук, Шкатов Д.П. (shkatov@gmail.com) - Университет Витвотерсранда, Йоханнесбург, Южная Африка, кандидат философских наук
Ключевые слова: вычислительная сложность, проблема разрешения, логика ветвящегося времени, темпоральные логики, неклассические логики, пропозициональные логики
Keywords: computational complexity, decision problem, computational tree logic, temporal logic, non-classical logics, propositional logics
Количество просмотров: 1756
Версия для печати
Выпуск в формате PDF (5.41Мб)
Скачать обложку в формате PDF (0.62Мб)

Размер шрифта:       Шрифт:

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

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

 

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


Постоянный адрес статьи:
http://swsys.ru/index.php?page=article&id=4230
Версия для печати
Выпуск в формате PDF (5.41Мб)
Скачать обложку в формате PDF (0.62Мб)
Статья опубликована в выпуске журнала № 4 за 2016 год. [ на стр. 135–142 ]

Возможно, Вас заинтересуют следующие статьи схожих тематик: