Выполнимость мю-исчисления с арифметическими ограничениями

Пропозициональное модальное $\mu$-исчисление является хорошо известным языком спецификаций систем помеченных переходов. В этой работе мы изучаем расширение этой логики с помощью обратных модальностей и арифметических ограничений Пресбургера, интерпретируемых на древовидных моделях. Мы описываем алгоритм выполнимости, основанный на построении по уровням моделей Фишера-Ларднера. Также сообщается о совместном выполнении нескольких экспериментов. Кроме того, мы описываем применение алгоритма для решения задач статического анализа полуструктурированных данных.