В теоретической информатике модальное μ-исчисление (Lμ, Lμ, иногда просто μ-исчисление, хотя это может иметь более общее значение) является расширением высказываний модальной логики (с многими модальностями ) посредством добавление оператора наименьшей фиксированной точки μ и оператора наибольшей фиксированной точки , таким образом, фиксированная точка логика.
(пропозициональное, модальное) μ-исчисление берет свое начало от Даны Скотт и было развито Декстером Козеном в наиболее используемую в настоящее время версию. Он используется для описания свойств помеченных переходных систем и для проверки этих свойств. Многие темпоральные логики могут быть закодированы в μ-исчислении, включая CTL * и его широко используемые фрагменты - линейная темпоральная логика и логика вычислительного дерева.
Алгебраическая точка зрения состоит в том, чтобы рассматривать его как алгебру из монотонных функций над полной решеткой с операторами, состоящими из функциональной композиции плюс операторы наименьшей и наибольшей фиксированной точки; с этой точки зрения модальное µ-исчисление находится над решеткой алгебры степенных множеств. игровая семантика μ-исчисления связана с играми для двух игроков с точной информацией, в частности с бесконечными играми на четность.
Содержание
- 1 Синтаксис
- 2 Обозначение семантики
- 3 Проблемы принятия решения
- 4 См. Также
- 5 Примечания
- 6 Ссылки
- 7 Внешние ссылки
Синтаксис
Пусть P (предложения) и A (действия) - два конечных набора символов, а V - счетно бесконечное множество переменных. Набор формул (пропозиционального, модального) μ-исчисления определяется следующим образом:
- каждое предложение и каждая переменная является формулой;
- если и - формулы, тогда - формула.
- если - формула, то - формула ;
- если - формула, а - действие, то - формула; (произносится либо: box или после обязательно )
- , если - формула, а - переменная, тогда - формула при условии, что каждый бесплатный ок. Величина в происходит положительно, то есть в рамках четного числа отрицаний.
(Понятия свободных и связанных переменных являются обычными, где - единственный оператор связывания.)
Учитывая приведенные выше определения, мы можем обогатите синтаксис:
- , что означает
- (произносится либо: ромб или после , возможно, ) означает
- означает , где означает замену на во всех свободных вхождениях из в .
Первые две формулы являются знакомыми по классическому исчислению высказываний и, соответственно, минимальной мультимодальной логике K.
Обозначение (и его двойственный) вдохновлены лямбда-исчислением ; цель состоит в том, чтобы обозначить наименьшую (и, соответственно, наибольшую) фиксированную точку выражения , где «минимизация» (и, соответственно, «максимизация») находится в переменной , как в лямбда-исчислении - функция с формулой в связанной переменной ; подробнее см. денотационную семантику ниже.
Денотационная семантика
Модели (пропозиционального) μ-исчисления представлены как помеченные переходные системы где:
- - набор состояний;
- карты к каждой метке бинарное отношение на ;
- , сопоставляет каждому предложению множество состояний, в которых утверждение истинно.
Дано маркированная система перехода и интерпретация переменные из -исчисление, - это функция, определяемая следующими правилами:
- ;
- ;
- ;
- ;
- ;
- , где сопоставляет с при сохранении отображений везде.
По двойственности интерпретация других базовых формул следующая:
- ;
- ;
Менее формально это означает, что для данной системы переходов :
- сохраняется в наборе состояний ;
- сохраняется в каждом состоянии, где и оба удерживаются;
- сохраняется в каждом состоянии, где не удерживается.
- удерживается в состоянии если каждый -переход, ведущий из , приводит к состоянию, где удерживается.
- удерживается в состоянии , если существует -переход, ведущий из , что приводит к состоянию, в котором выполняется .
- удерживается в любом состоянии в любом наборе , так что когда переменная имеет значение , затем сохраняется для всех . (Из теоремы Кнастера – Тарского следует, что - наибольшая фиксированная точка в и его наименьшая фиксированная точка.)
Интерпретации и на самом деле являются «классическими» из динамической логики. Кроме того, оператор можно интерпретировать как живучесть («что-то хорошее со временем произойдет») и как («ничего плохого никогда не случится») в Неофициальная классификация Лесли Лэмпорта.
Примеры
- интерпретируется как «истинно для каждого a-пути». Идентификатор ea заключается в том, что "истинно на каждом пути" может быть определено аксиоматически как это (самое слабое) предложение , что подразумевает и остается верным после обработки любой a-метки.
- интерпретируется как наличие пути вдоль a-переходов в состояние, где holds.
- Свойство системы быть тупиковой -свободной, что означает отсутствие состояний без исходящих переходов и, кроме того, что путь к такому состояние не существует, выражается формулой
Проблемы принятия решения
Выполнимость формулы модального μ-исчисления EXPTIME-complete. Что касается линейной временной логики, проблемы проверки модели, выполнимости и достоверности линейного модального μ-исчисления являются PSPACE-complete.
См. Также
Примечания
- ^Скотт, Дана; Баккер, Якобус (1969). «Теория программ». Неопубликованная рукопись.
- ^Kozen, Dexter (1982). «Результаты по μ-исчислению высказываний». Автоматы, языки и программирование. ИКАЛП. 140 . С. 348–359. doi : 10.1007 / BFb0012782. ISBN 978-3-540-11576-2.
- ^Кларк с.108, теорема 6; Эмерсон П. 196
- ^Арнольд и Нивинский, стр. Viii-x и глава 6
- ^Арнольд и Нивиньский, стр. Viii-x и глава 4
- ^Арнольд и Нивинский, стр. 14
- ^ Брэдфилд и Стирлинг, стр. 731
- ^Брэдфилд и Стирлинг, стр. 6
- ^ Эрих Гредель; Фокион Г. Колайтис; Леонид Либкин ; Маартен Маркс; Джоэл Спенсер; Моше Й. Варди; Yde Venema; Скотт Вайнштейн (2007). Теория конечных моделей и ее приложения. Springer. п. 159. ISBN 978-3-540-00428-8.
- ^Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы. Springer. п. 521. ISBN 978-3-540-00296-3.
- ^Sistla, A. P.; Кларк, Э. М. (1 июля 1985 г.). «Сложность пропозициональной линейной темпоральной логики». J. ACM. 32 (3): 733–749. DOI : 10.1145 / 3828.3837. ISSN 0004-5411.
- ^Варди, М. Ю. (1988-01-01). "Временное исчисление фиксированных точек". Материалы 15-го Симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования. ПОПЛ '88. Нью-Йорк, Нью-Йорк, США: ACM: 250–259. doi : 10.1145 / 73560.73582. ISBN 0897912527.
Ссылки
- Clarke, Jr., Edmund M.; Орна Грумберг; Дорон А. Пелед (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