Journal influence
Higher Attestation Commission (VAK) - К1 quartile
Russian Science Citation Index (RSCI)
Bookmark
Next issue
№4
Publication date:
09 December 2024
Algorithmic undecidability of the problem of first-order correspondence of computational tree logic formulas
Date of submission article: 21.03.2018
UDC: 510.53, 510.643
The article was published in issue no. № 3, 2018 [ pp. 591-597 ]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.
Аннотация:В качестве формального средства, описывающего свойства различных структур (в том числе структур вычислений), обычно используют язык логики предикатов. Этот язык, с одной стороны, понятен и удобен, а с другой, многие вопросы, важные с прикладной точки зрения, для него алгоритмически неразрешимы, то есть не могут быть решены программно. Сейчас существует много альтернативных языков, позволяющих описывать вычисления и их свойства, при этом, в отличие от языка логики предикатов, аналогичные вопросы для них алгоритмически разрешимы. В работе рассматривается один из таких языков – язык логики ветвящегося времени CTL. Он используется для верификации программ, так как содержит средства для описания свойств программных вычислений, в частности, свойств бинарного отношения, возникающего в реляционной семантике Крипке. В работе исследуется возможность алгоритмического нахождения формул языка первого порядка, которые задают те же классы шкал Крипке, что и формулы языка логики CTL. Известно, что для интуицинистских формул проблема их первопорядковой определимости алгоритмически неразрешима. Показано, как, используя перевод Гёделя интуиционистских формул в модальные, а затем перевод получившихся модальных формул в формулы языка логики CTL, свести проблему первопорядковой определимости интуиционистских формул на шкалах Крипке к проблеме первопопорядковой определимости CTL-формул на шкалах Крипке. В качестве следствия такого сведения получена алгоритмическая неразрешимость соответствующей проблемы для CTL. В заключении обсуждаются возможные модификации приведенной конструкции с целью распространения полученного результата на фрагменты языка логики CTL, а также алгоритмическая разрешимость проблемы CTL-определимости формул первого порядка.
| Authors: M.N. Rybakov (m_rybakov@mail.ru) - Tver State University, R&D Institute Centerprogramsystem (Associate Professor, Software Engineer, Research Fellow), Tver, Russia, Ph.D, L.A. Chagrova (chagrovy@mail.ru) - Tver State University (Associate Professor), Tver, Russia, Ph.D | |
| Keywords: computational models, computational tree logic, first-order definability |
|
| Page views: 4688 |
PDF version article Full issue in PDF (29.03Mb) |
Язык логики ветвящегося времени CTL (computational tree logic) – удобное и эффективное средство для описания свойств различных сложных вычислительных систем, в том числе с целью их последующей верификации [1, 2]. Его существенным отличием от хорошо известного и широко используемого языка логики предикатов QCL является то, что важные для прикладного аспекта задачи общезначимости и выполнимости CTL-формул разрешимы [3], в то время как для проблем тождественной истинности и выполнимости формул языка логики QCL разрешающей процедуры не существует в принципе [4]. Оба языка позволяют описывать свойства (серийного) бинарного отношения: свойства отношения достижимости в шкалах Крипке для CTL, с одной стороны, могут быть описаны с помощью модальностей языка CTL, а с другой – с помощью формул языка логики предикатов, содержащих предикатную букву |
| Permanent link: http://swsys.ru/index.php?id=4504&lang=en&page=article |
Print version Full issue in PDF (29.03Mb) |
| The article was published in issue no. № 3, 2018 [ pp. 591-597 ] |
Perhaps, you might be interested in the following articles of similar topics:
