|
Выполнимость мю-исчисления с арифметическими ограничениями
Й. Лимонa, Э. Барсенасb, Э. Бенитес-Геррероa, Г. Молеро-Кастильоb, А. Веласкес Менаb a Университет Веракрузана
b Национальный автономный университет Мексики
Аннотация:
Пропозициональное модальное $\mu$-исчисление является хорошо известным языком спецификаций систем помеченных переходов. В этой работе мы изучаем расширение этой логики с помощью обратных модальностей и арифметических ограничений Пресбургера, интерпретируемых на древовидных моделях. Мы описываем алгоритм выполнимости, основанный на построении по уровням моделей Фишера-Ларднера. Также сообщается о совместном выполнении нескольких экспериментов. Кроме того, мы описываем применение алгоритма для решения задач статического анализа полуструктурированных данных.
Ключевые слова:
модальные логики, автоматизированное построение логического вывода, формальная верификация, пресбургеровская арифметика, полуструктурированные данные.
Образец цитирования:
Й. Лимон, Э. Барсенас, Э. Бенитес-Герреро, Г. Молеро-Кастильо, А. Веласкес Мена, “Выполнимость мю-исчисления с арифметическими ограничениями”, Труды ИСП РАН, 33:2 (2021), 191–200
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tisp594 https://www.mathnet.ru/rus/tisp/v33/i2/p191
|
Статистика просмотров: |
Страница аннотации: | 105 | PDF полного текста: | 38 | Список литературы: | 20 |
|