В теоретической информатике , то модальное μ-исчисление ( Lμ , L μ , иногда просто μ-исчисление , хотя это может иметь более общее значение) является расширением пропозициональной модальной логики (с многими условиями ) путем добавления мере неподвижную точку оператора μ и оператор наибольшей неподвижной точки, таким образом, логика с фиксированной точкой .
В (пропозициональном, модальном) μ-исчисление берет свое начало с Даной Скотт и Жако де Баккер , [1] и в дальнейшем было разработано Dexter Közen [2] в версию наиболее часто используемый в настоящее время. Он используется для описания свойств помеченных переходных систем и для проверки этих свойств. Многие временные логики могут быть закодированы в μ-исчислении, включая CTL * и его широко используемые фрагменты - линейную временную логику и логику вычислительного дерева . [3]
Алгебраическое взгляд , чтобы увидеть его в качестве алгебры из монотонных функций над полной решеткой , с операторами , состоящих из функциональной композиции плюс наималейшими и наибольшими операторами фиксированной точки; с этой точки зрения модальное μ-исчисление находится над решеткой алгебры степенных множеств . [4] В игре семантика из мю-исчисления связана с двумя игроков с полной информацией , в частности бесконечных игр четности . [5]
Синтаксис
Пусть P (предложения) и A (действия) - два конечных набора символов, а Var - счетно бесконечное множество переменных. Набор формул (пропозиционального, модального) μ-исчисления определяется следующим образом:
- каждое предложение и каждая переменная - это формула;
- если а также формулы, то это формула;
- если формула, то это формула;
- если формула и это действие, то это формула; (произносится либо: коробка или после обязательно )
- если формула и переменная, тогда является формулой при условии, что каждое свободное вхождение в происходит положительно, т.е. в рамках четного числа отрицаний.
(Понятия свободных и связанных переменных как обычно, где - единственный оператор привязки.)
Учитывая приведенные выше определения, мы можем обогатить синтаксис:
- имея в виду
- (произносится либо: алмаз или после возможно ) имея в виду
- средства , где означает замену для во всех свободных вхождений в в .
Первые две формул знакомые одни из классического исчисления высказываний и , соответственно , минимальная мультимодальные логики K .
Обозначение (и его дуал) вдохновлены лямбда-исчислением ; цель состоит в том, чтобы обозначить наименьшую (и, соответственно, наибольшую) неподвижную точку выражения где «минимизация» (и, соответственно, «максимизация») находятся в переменной , как в лямбда-исчислении функция с формулой в связанной переменной ; [6] подробности см. В денотационной семантике ниже.
Денотационная семантика
Модели (пропозиционального) μ-исчисления представлены в виде помеченных переходных систем. где:
- это набор состояний;
- сопоставляется с каждой меткой бинарное отношение на ;
- , отображает каждое предложение к множеству состояний, в которых утверждение верно.
Учитывая помеченную переходную систему и интерпретация переменных принадлежащий -исчисление, , это функция, определяемая следующими правилами:
- ;
- ;
- ;
- ;
- ;
- , где карты к при сохранении отображений где-либо еще.
По двойственности интерпретация других основных формул такова:
- ;
- ;
Менее формально это означает, что для данной переходной системы :
- выполняется во множестве состояний ;
- выполняется в каждом состоянии, где а также оба держатся;
- выполняется в каждом состоянии, где не держит.
- держит в состоянии если каждый -переход, ведущий из приводит к состоянию, когда держит.
- держит в состоянии если существует -переход, ведущий из что приводит к состоянию, когда держит.
- выполняется в любом состоянии в любом наборе так что, когда переменная установлен на , тогда относится ко всем . (Из теоремы Кнастера – Тарского следует, чтоэто самая большая фиксированная точка из, а также его наименьшая фиксированная точка .)
Интерпретации а также на самом деле являются «классическими» из динамической логики . Дополнительно операторможно интерпретировать как живость («в конце концов что-то хорошее случается») икак безопасность («ничего плохого никогда не бывает») в неофициальной классификации Лесли Лэмпорта . [7]
Примеры
- интерпретируется как "Правда вместе с каждым в -path « [7] Идея состоит в том , что»истинно вдоль каждого в -path»может быть определен аксиоматический как то (самыми слабыми) предложения что подразумевает и который остается верным после обработки любого в -label. [8]
- интерпретируется как существование пути вдоль через -переходов в состояние , гдедержит. [9]
- Свойство системы быть свободным от тупиков , то есть не иметь состояний без исходящих переходов и, кроме того, не существует пути к такому состоянию, выражается формулой [9]
Проблемы с решением
Выполнимость модальной формулы μ-исчисления является EXPTIME-полной . [10] Что касается линейной временной логики, [11] проблемы проверки модели, выполнимости и достоверности линейного модального μ-исчисления являются PSPACE-полными . [12]
Смотрите также
- Теория конечных моделей
- Модальное μ-исчисление без чередования
Заметки
- ^ Скотт, Дана ; Баккер, Якобус (1969). «Теория программ». Неопубликованная рукопись .
- ^ Козен, Декстер (1982). «Результаты по μ-исчислению высказываний». Автоматы, языки и программирование . ИКАЛП. 140 . С. 348–359. DOI : 10.1007 / BFb0012782 . ISBN 978-3-540-11576-2.
- ^ Кларк стр.108, теорема 6; Эмерсон П. 196
- ↑ Арнольд и Нивинский, стр. Viii-x и глава 6
- ↑ Арнольд и Нивинский, стр. Viii-x и глава 4
- ↑ Арнольд и Нивинский, стр. 14
- ^ a b Брэдфилд и Стирлинг, стр. 731
- ^ Брэдфилд и Стирлинг, стр. 6
- ^ а б Эрих Гредель; Фокион Г. Колайтис; Леонид Либкин ; Маартен Маркс; Джоэл Спенсер ; Моше Й. Варди ; Yde Venema; Скотт Вайнштейн (2007). Теория конечных моделей и ее приложения . Springer. п. 159. ISBN. 978-3-540-00428-8.
- ^ Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы . Springer. п. 521. ISBN. 978-3-540-00296-3.
- ^ Sistla, AP; Кларк, EM (1985-07-01). «Сложность пропозициональной линейной темпоральной логики». J. ACM . 32 (3): 733–749. DOI : 10.1145 / 3828.3837 . ISSN 0004-5411 .
- ^ Варди, MY (1988-01-01). «Временное исчисление точек фиксации». Материалы 15-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . ПОПЛ '88. Нью-Йорк, Нью-Йорк, США: ACM: 250–259. DOI : 10.1145 / 73560.73582 . ISBN 0897912527.
Рекомендации
- Кларк младший, Эдмунд М .; Орна Грумберг; Дорон А. Пелед (1999). Проверка модели . Кембридж, Массачусетс, США: MIT press. ISBN 0-262-03270-8., глава 7, Проверка моделей для μ-исчисления, стр. 97–108
- Стирлинг, Колин. (2001). Модальные и временные свойства процессов . Нью-Йорк, Берлин, Гейдельберг: Springer Verlag. ISBN 0-387-98717-7., глава 5, Модальное µ-исчисление, стр. 103–128
- Андре Арнольд; Дамиан Нивинский (2001). Зачатки μ-исчисления . Эльзевир. ISBN 978-0-444-50620-7., глава 6, μ-исчисление над алгебрами степенных множеств, стр. 141–153 посвящена модальному μ-исчислению.
- Иде Венема (2008) Лекции по модальному μ-исчислению ; был представлен на 18-й Европейской летней школе по логике, языку и информации
- Брэдфилд, Джулиан и Стирлинг, Колин (2006). «Модальные му-исчисления» . У П. Блэкберна; J. van Benthem & F. Wolter (ред.). Справочник по модальной логике . Эльзевир . С. 721–756.
- Эмерсон, Э. Аллен (1996). «Проверка моделей и Мю-исчисление». Описательная сложность и конечные модели . Американское математическое общество . С. 185–214. ISBN 0-8218-0517-7.
- Козен, Декстер (1983). «Результаты по μ-исчислению высказываний». Теоретическая информатика . 27 (3): 333–354. DOI : 10.1016 / 0304-3975 (82) 90125-6 .
Внешние ссылки
- Софи Пинчинат, « Логика, автоматы и игры», видеозапись лекции на Летней школе логики ANU '09