RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2018, том 25, номер 5, страницы 506–524 (Mi mais645)  

Прикладные логики

О выразительных возможностях некоторых расширений линейной темпоральной логики

А. Р. Гнатенкоa, В. А. Захаровb

a Московский государственный университет им. М.В. Ломоносова, Ленинские горы, 1, г. Москва, 119991 Россия
b Национальный исследовательский университет «Высшая школа экономики», ул. Мясницкая, 20, г. Москва, 101000 Россия

Аннотация: Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Мы полагаем, что для формального описания поведения реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционная темпоральная логика линейного времени $LTL$. В этой работе рассматривается новый язык формальных спецификаций $\mathcal{LP}$-$LTL$, представляющий собой расширение темпоральной логики $LTL$, специально разработанное для описания свойств вычислений автоматов-преобразователей. Темпоральные операторы в формулах $\mathcal{LP}$-$LTL$ снабжены параметрами, в качестве которых используются множества слов (языки), описывающие потоки сигналов управления, поступающих на вход реагирующей системы. Базовые предикаты в формулах $\mathcal{LP}$-$LTL$ также определяются языками в алфавите элементарных действий; эти языки описывают ожидаемую реакцию системы в ответ на воздействия окружающей среды. В более ранних работах авторов этой статьи изучалась задача верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами логик $\mathcal{LP}$-$LTL$ и $\mathcal{LP}$-$CTL$. Было показано, что для обеих логик эта задача алгоритмически разрешима. Цель данной работы — оценить выразительные возможности логики $\mathcal{LP}$-$LTL$ и сравнить ее с широко известными логиками, применяющимися в информатике для спецификации реагирующих систем. В логике $\mathcal{LP}$-$LTL$ были выделены два фрагмента $\mathcal{LP}$-$1$-$LTL$ и $\mathcal{LP}$-$n$-$LTL$. Нам удалось установить, что язык спецификаций $\mathcal{LP}$-$1$-$LTL$ более выразителен, чем $LTL$, в то время как фрагмент $\mathcal{LP}$-$n$-$LTL$ обладает точно такими же выразительными возможностями, что и монадическая логика второго порядка S$1$S.

Ключевые слова: темпоральные логики, выразительность, спецификация, верификация, автоматы Бюхи, бесконечные слова.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 18-01-00854_а
Работа выполнена при финансовой поддержке гранта РФФИ N 18-01-00854.


DOI: https://doi.org/10.18255/1818-1015-506-524

Полный текст: PDF файл (683 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 517.9
Поступила в редакцию: 10.09.2018

Образец цитирования: А. Р. Гнатенко, В. А. Захаров, “О выразительных возможностях некоторых расширений линейной темпоральной логики”, Модел. и анализ информ. систем, 25:5 (2018), 506–524

Цитирование в формате AMSBIB
\RBibitem{GnaZak18}
\by А.~Р.~Гнатенко, В.~А.~Захаров
\paper О выразительных возможностях некоторых расширений линейной темпоральной логики
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 5
\pages 506--524
\mathnet{http://mi.mathnet.ru/mais645}
\crossref{https://doi.org/10.18255/1818-1015-506-524}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais645
  • http://mi.mathnet.ru/rus/mais/v25/i5/p506

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:34
    Полный текст:8
    Литература:4
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019