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

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

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



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






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


Модел. и анализ информ. систем, 2021, том 28, номер 1, страницы 104–119 (Mi mais738)  

Theory of computing

LTL-спецификация счётчиковых машин

Е. В. Кузьмин

Ярославский государственный университет им. П. Г. Демидова, ул. Советская, д. 14, г. Ярославль, 150003 Россия

Аннотация: Статья написана в поддержку учебной дисциплины “Неклассические логики”. В рамках этой дисциплины объектами изучения являются базовые принципы и конструктивные элементы, с помощью которых происходит формальное построение различных неклассических логик высказываний. Несмотря на абстрактность теории неклассических логик, в которой основное внимание уделяется строгой математической формализации логических рассуждений, существуют реальные прикладные области применения теоретических результатов. В частности, языки темпоральных модальных логик широко используются для моделирования, спецификации и верификации (анализа корректности) программных систем логического управления. В этой статье на примере линейной темпоральной логики LTL демонстрируется, как абстрактные понятия неклассических логик могут находить отражение на практике в области информационных технологий и программирования. Показывается возможность представления поведения программной системы в виде набора LTL-формул и использования этого представления для проверки выполнимости программных свойств системы через процедуру доказательства справедливости логических выводов, выраженных в терминах линейной темпоральной логики LTL. В качестве программных систем, для спецификации поведения которых будет применяться логика LTL, рассматриваются счётчиковые машины Минского. Счётчиковые машины Минского - один из способов формализации интуитивного понятия алгоритма. Они обладают той же вычислительной мощностью, что и машины Тьюринга. Счётчиковая машина имеет вид компьютерной программы, написанной на языке высокого уровня, поскольку содержит переменные, называемые счётчиками, и операторы условного и безусловного перехода, позволяющие строить конструкции циклов. Известно, что любой алгоритм (гипотетически) может быть реализован в виде трёхсчётчиковой машины Минского.

Ключевые слова: неклассическая логика, линейная темпоральная логика, счётчиковые машины, LTL-спецификация.

Финансовая поддержка
Работа выполнена в рамках инициативной НИР ЯрГУ им. П. Г. Демидова № VIP-016.


DOI: https://doi.org/10.18255/1818-1015-2021-1-104-119

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

Тип публикации: Статья
УДК: 519.7
MSC: 68Q60, 68N30, 68Q04, 03B44, 03B70, 03D10
Поступила в редакцию: 11.01.2021
Исправленный вариант: 12.02.2021
Принята в печать:12.03.2021

Образец цитирования: Е. В. Кузьмин, “LTL-спецификация счётчиковых машин”, Модел. и анализ информ. систем, 28:1 (2021), 104–119

Цитирование в формате AMSBIB
\RBibitem{Kuz21}
\by Е.~В.~Кузьмин
\paper LTL-спецификация счётчиковых машин
\jour Модел. и анализ информ. систем
\yr 2021
\vol 28
\issue 1
\pages 104--119
\mathnet{http://mi.mathnet.ru/mais738}
\crossref{https://doi.org/10.18255/1818-1015-2021-1-104-119}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais738
  • http://mi.mathnet.ru/rus/mais/v28/i1/p104

    ОТПРАВИТЬ: 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
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:15
    Полный текст:4
     
    Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2021