Авторитетность издания
ВАК - К1
RSCI, ядро РИНЦ
Добавить в закладки
Следующий номер на сайте
№4
Ожидается:
09 Декабря 2024
Алгоритмическая неразрешимость проблемы первопорядковой определимости формул логики ветвящегося времени
Algorithmic undecidability of the problem of first-order correspondence of computational tree logic formulas
Дата подачи статьи: 21.03.2018
УДК: 510.53, 510.643
Статья опубликована в выпуске журнала № 3 за 2018 год. [ на стр. 591-597 ]Аннотация:В качестве формального средства, описывающего свойства различных структур (в том числе структур вычислений), обычно используют язык логики предикатов. Этот язык, с одной стороны, понятен и удобен, а с другой, многие вопросы, важные с прикладной точки зрения, для него алгоритмически неразрешимы, то есть не могут быть решены программно. Сейчас существует много альтернативных языков, позволяющих описывать вычисления и их свойства, при этом, в отличие от языка логики предикатов, аналогичные вопросы для них алгоритмически разрешимы. В работе рассматривается один из таких языков – язык логики ветвящегося времени CTL. Он используется для верификации программ, так как содержит средства для описания свойств программных вычислений, в частности, свойств бинарного отношения, возникающего в реляционной семантике Крипке. В работе исследуется возможность алгоритмического нахождения формул языка первого порядка, которые задают те же классы шкал Крипке, что и формулы языка логики CTL. Известно, что для интуицинистских формул проблема их первопорядковой определимости алгоритмически неразрешима. Показано, как, используя перевод Гёделя интуиционистских формул в модальные, а затем перевод получившихся модальных формул в формулы языка логики CTL, свести проблему первопорядковой определимости интуиционистских формул на шкалах Крипке к проблеме первопопорядковой определимости CTL-формул на шкалах Крипке. В качестве следствия такого сведения получена алгоритмическая неразрешимость соответствующей проблемы для CTL. В заключении обсуждаются возможные модификации приведенной конструкции с целью распространения полученного результата на фрагменты языка логики CTL, а также алгоритмическая разрешимость проблемы CTL-определимости формул первого порядка.
Abstract:It is common to use the first-order language as a formal tool for describing properties of various (computational) structures. On the one hand, this language is well understood and easy to use; on the other, many questions that are im-portant from the applications point of view related to this language are algorithmically undecidable, i.e., cannot be answered using a computer program. These days, there exist various alternative languages that can be used for describing computational processes and their properties, for which the corresponding questions are, in contrast to the first-order language, algorithmically decidable. In this paper, we consider one of such languages, – the language of the Computational Tree Logic (CTL). It is commonly used for program verification as it is capable of describing properties of computational processes, – in particular, properties of the binary relation used in the Kripke semantics. The authors investigate the possibility of finding algorithmically first-order formulas defining the same classes of Kripke frames as the formulas of the language of CTL. It is well known the problem of finding first-order correspondents of propositional intuitionistic formulas is algorithmically undecidable. The authors reduce – using the Gödel translation of intuitionistic formulas into modal ones, and subsequently a translation of resultant modal formulas into CTL-formulas – the first-order correspondence problem for propositional intuitionistic formulas to the first-order correspondence problem for CTL-formulas on Kripke frames. As a result of this reduction, they prove that the first-order correspondence problem for CTL-formulas is algorithmically undecidable. In the conclusion, the authors discuss some possible modifications of their construction for fragments of the language of CTL as well as algorithmic decidability of the CTL correspondence problem for first-order formulas.
| Авторы: Рыбаков М.Н. (m_rybakov@mail.ru) - Тверской государственный университет; НИИ «Центрпрограммсистем»; Университет Витвотерсранда (доцент, инженер-программист, научный сотрудник), Тверь, Россия, кандидат физико-математических наук, Чагрова Л.А. (chagrovy@mail.ru) - Тверской государственный университет (доцент), Тверь, Россия, кандидат физико-математических наук | |
| Ключевые слова: модели вычислений, логика ветвящегося времени, первопорядковая определимость |
|
| Keywords: computational models, computational tree logic, first-order definability |
|
| Количество просмотров: 4689 |
Статья в формате PDF Выпуск в формате PDF (29.03Мб) |
Язык логики ветвящегося времени CTL (computational tree logic) – удобное и эффективное средство для описания свойств различных сложных вычислительных систем, в том числе с целью их последующей верификации [1, 2]. Его существенным отличием от хорошо известного и широко используемого языка логики предикатов QCL является то, что важные для прикладного аспекта задачи общезначимости и выполнимости CTL-формул разрешимы [3], в то время как для проблем тождественной истинности и выполнимости формул языка логики QCL разрешающей процедуры не существует в принципе [4]. Оба языка позволяют описывать свойства (серийного) бинарного отношения: свойства отношения достижимости в шкалах Крипке для CTL, с одной стороны, могут быть описаны с помощью модальностей языка CTL, а с другой – с помощью формул языка логики предикатов, содержащих предикатную букву |
| Постоянный адрес статьи: http://swsys.ru/index.php?id=4504&page=article |
Версия для печати Выпуск в формате PDF (29.03Мб) |
| Статья опубликована в выпуске журнала № 3 за 2018 год. [ на стр. 591-597 ] |
Возможно, Вас заинтересуют следующие статьи схожих тематик:
