Модальное μ-исчисление

В теоретической информатике модальное μ-исчисление ( Lμ , L _μ , иногда просто μ-исчисление , хотя это может иметь более общий смысл) является расширением пропозициональной модальной логики (со многими модальностями ) путём добавления наименьшей фиксированной точки оператора . µ и оператор наибольшей неподвижной точки ν, таким образом, логика неподвижной точки .

(Пропозициональное, модальное) μ-исчисление берет свое начало от Даны Скотт и Жако де Баккера . ^[1] и был далее развит Декстером Козеном. ^[2] в наиболее используемую в настоящее время версию. Он используется для описания свойств меченых переходных систем и проверки этих свойств. Многие темпоральные логики могут быть закодированы в μ-исчислении, включая CTL* и его широко используемые фрагменты — линейную темпоральную логику и логику вычислительного дерева . ^[3]

Алгебраический взгляд состоит в том, чтобы рассматривать ее как алгебру монотонных функций над полной решеткой с операторами, состоящими из функциональной композиции плюс операторы наименьшего и наибольшего неподвижной точки; с этой точки зрения модальное µ-исчисление находится над решеткой алгебры степенного множества . ^[4] Игровая семантика μ-исчисления связана с играми для двух игроков с совершенной информацией , особенно с играми с бесконечной четностью . ^[5]

Синтаксис

Пусть P (предложения) и A (действия) — два конечных набора символов, и пусть Var — счетный бесконечный набор переменных. Множество формул (пропозиционального, модального) µ-исчисления определяется следующим образом:

каждое предложение и каждая переменная — это формула;
если $\phi$ и $\psi$ являются формулами, то $\phi \wedge \psi$ это формула;
если $\phi$ это формула, то $\neg \phi$ это формула;
если $\phi$ это формула и $a$ это действие, то $[a]\phi$ это формула; (произносится либо: $a$ коробка $\phi$ или после $a$ обязательно $\phi$ )
если $\phi$ это формула и $Z$ переменная, то $\nu Z.\phi$ является формулой при условии, что каждое свободное вхождение $Z$ в $\phi$ происходит положительно, т. е. в пределах четного числа отрицаний.

(Понятия свободных и связанных переменных остаются обычными, где $\nu$ является единственным оператором привязки.)

Учитывая приведенные выше определения, мы можем дополнить синтаксис:

$\phi \lor \psi$ значение $\neg (\neg \phi \land \neg \psi )$
$\langle a\rangle \phi$ (произносится либо: $a$ алмаз $\phi$ или после $a$ возможно $\phi$ ) значение $\neg [a]\neg \phi$
$\mu Z.\phi$ означает $\neg \nu Z.\neg \phi [Z:=\neg Z]$ , где $\phi [Z:=\neg Z]$ означает замену $\neg Z$ для $Z$ во всех свободных случаях $Z$ в $\phi$ .

Первые две формулы известны из классического исчисления высказываний из минимальной мультимодальной логики K. и, соответственно ,

Обозначения $\mu Z.\phi$ (и его двойник) основаны на лямбда-исчислении ; цель состоит в том, чтобы обозначить наименьшую (и, соответственно, наибольшую) фиксированную точку выражения $\phi$ где «минимизация» (и соответственно «максимизация») находятся в переменной $Z$ , очень похоже на лямбда-исчисление $\lambda Z.\phi$ это функция с формулой $\phi$ в связанной переменной $Z$ ; ^[6] подробности см. в денотационной семантике ниже.

Денотационная семантика

Модели (пропозиционального) μ-исчисления представлены как помеченные переходные системы. $(S,R,V)$ где:

$S$ представляет собой набор состояний;
$R$ карты для каждой метки $a$ бинарное отношение на $S$ ;
$V:P\to 2^{S}$ , отображает каждое предложение $p\in P$ к множеству состояний, в которых предложение истинно.

Учитывая помеченную систему перехода $(S,R,V)$ и интерпретация $i$ переменных $Z$ принадлежащий $\mu$ -исчисление, $[\![\cdot ]\!]_{i}:\phi \to 2^{S}$ , — это функция, определяемая следующими правилами:

$[\![p]\!]_{i}=V(p)$ ;
$[\![Z]\!]_{i}=i(Z)$ ;
$[\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}$ ;
$[\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{i}$ ;
$[\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}$ ;
$[\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}$ , где $i[Z:=T]$ карты $Z$ к $T$ сохраняя при этом отображения $i$ везде еще.

В соответствии с двойственностью интерпретация остальных основных формул такова:

$[\![\phi \vee \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cup [\![\psi ]\!]_{i}$ ;
$[\![\langle a\rangle \phi ]\!]_{i}=\{s\in S\mid \exists t\in S,(s,t)\in R_{a}\wedge t\in [\![\phi ]\!]_{i}\}$ ;
$[\![\mu Z.\phi ]\!]_{i}=\bigcap \{T\subseteq S\mid [\![\phi ]\!]_{i[Z:=T]}\subseteq T\}$

Менее формально это означает, что для данной переходной системы $(S,R,V)$ :

$p$ содержится в множестве состояний $V(p)$ ;
$\phi \wedge \psi$ имеет место в каждом штате, где $\phi$ и $\psi$ оба держатся;
$\neg \phi$ имеет место в каждом штате, где $\phi$ не держит.
$[a]\phi$ держит в состоянии $s$ если каждый $a$ -переход, ведущий из $s$ приводит к состоянию, когда $\phi$ держит.
$\langle a\rangle \phi$ держит в состоянии $s$ если существует $a$ -переход, ведущий из $s$ что приводит к состоянию, когда $\phi$ держит.
$\nu Z.\phi$ выполняется в любом состоянии в любом множестве $T$ так что, когда переменная $Z$ установлено на $T$ , затем $\phi$ сохраняется для всех $T$ . (Из теоремы Кнастера–Тарского следует, что $[\![\nu Z.\phi ]\!]_{i}$ является наибольшей неподвижной точкой $T\mapsto [\![\phi ]\!]_{i[Z:=T]}$ , и $[\![\mu Z.\phi ]\!]_{i}$ его наименее фиксированная точка .)

Интерпретации $[a]\phi$ и $\langle a\rangle \phi$ на самом деле являются «классическими» из динамической логики . Кроме того, оператор $\mu$ можно интерпретировать как живость («со временем происходит что-то хорошее») и $\nu$ как безопасность («ничего плохого никогда не происходит») в Лесли Лэмпорта . неформальной классификации ^[7]

Примеры

$\nu Z.\phi \wedge [a]Z$ интерпретируется как « $\phi$ верно на каждом пути ". ^[7] Идея в том, что " $\phi$ истинно на каждом пути » может быть определено аксиоматически как это (самое слабое) предложение $Z$ что подразумевает $\phi$ и которое остается истинным после обработки любой -метки . ^[8]
$\mu Z.\phi \vee \langle a\rangle Z$ интерпретируется как существование пути по -переходам в состояние, где $\phi$ держит. ^[9]
Свойство состояния быть свободным от тупиков , то есть ни один путь из этого состояния не заходит в тупик, выражается формулой ^[9] $\nu Z.\left(\bigvee _{a\in A}\langle a\rangle \top \wedge \bigwedge _{a\in A}[a]Z\right)$

Проблемы с решением

Выполнимость модальной формулы μ-исчисления EXPTIME-полна . ^[10] Как и в случае с линейной темпоральной логикой, ^[11] проблемы проверки модели , выполнимости и достоверности линейного модального μ-исчисления являются PSPACE-полными . ^[12]

См. также

Примечания

^ Скотт, Дана ; Баккер, Якобус (1969). «Теория программ». Неопубликованная рукопись .
^ Козен, Декстер (1982). «Результаты по пропозициональному μ-исчислению». Автоматы, языки и программирование . ИКП. Том. 140. стр. 348–359. дои : 10.1007/BFb0012782 . ISBN 978-3-540-11576-2 .
^ Кларк стр.108, Теорема 6; Эмерсон стр. 196
^ Арнольд и Нивински, стр. viii-x и глава 6.
^ Арнольд и Нивински, стр. viii-x и глава 4.
^ Арнольд и Нивински, с. 14
^ Перейти обратно: ^а ^б Брэдфилд и Стерлинг, с. 731
^ Брэдфилд и Стерлинг, с. 6
^ Перейти обратно: ^а ^б Эрих Гредель; Фокион Г. Колайтис; Леонид Либкин ; Мартен Маркс; Джоэл Спенсер ; Моше Ю. Варди ; Иде Венема; Скотт Вайнштейн (2007). Теория конечных моделей и ее приложения . Спрингер. п. 159. ИСБН 978-3-540-00428-8 .
^ Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы . Спрингер. п. 521. ИСБН 978-3-540-00296-3 .
^ Систла, АП; Кларк, Э.М. (1 июля 1985 г.). «Сложность пропозициональной линейной темпоральной логики» . Дж. АКМ . 32 (3): 733–749. дои : 10.1145/3828.3837 . ISSN 0004-5411 .
^ Варди, МЮ (1 января 1988 г.). «Исчисление временных фиксированных точек». Материалы 15-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '88 . Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 250–259. дои : 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). «Модальные мю-исчисления» . В П. Блэкберне; Дж. ван Бентем и Ф. Вольтер (ред.). Справочник модальной логики . Эльзевир . стр. 721–756.
Эмерсон, Э. Аллен (1996). «Проверка модели и Му-исчисление». Описательная сложность и конечные модели . Американское математическое общество . стр. 185–214. ISBN 0-8218-0517-7 .
Козен, Декстер (1983). «Результаты по пропозициональному μ-исчислению». Теоретическая информатика . 27 (3): 333–354. дои : 10.1016/0304-3975(82)90125-6 .

Внешние ссылки

Софи Пинчина, «Логика, автоматы и игры», видеозапись лекции на Летней школе логики ANU '09

[1] Скотт, Дана ; Баккер, Якобус (1969). «Теория программ». Неопубликованная рукопись .

[Kozen1982-2] Козен, Декстер (1982). «Результаты по пропозициональному μ-исчислению». Автоматы, языки и программирование . ИКП. Том. 140. стр. 348–359. дои : 10.1007/BFb0012782 . ISBN 978-3-540-11576-2 .

[3] Кларк стр.108, Теорема 6; Эмерсон стр. 196

[4] Арнольд и Нивински, стр. viii-x и глава 6.

[5] Арнольд и Нивински, стр. viii-x и глава 4.

[6] Арнольд и Нивински, с. 14

[Bradfield_and_Stirling,_p._731-7] Перейти обратно: ^а ^б Брэдфилд и Стерлинг, с. 731

[8] Брэдфилд и Стерлинг, с. 6

[GrädelKolaitis2007-9] Перейти обратно: ^а ^б Эрих Гредель; Фокион Г. Колайтис; Леонид Либкин ; Мартен Маркс; Джоэл Спенсер ; Моше Ю. Варди ; Иде Венема; Скотт Вайнштейн (2007). Теория конечных моделей и ее приложения . Спрингер. п. 159. ИСБН 978-3-540-00428-8 .

[Schneider2004-10] Клаус Шнайдер (2004). Верификация реактивных систем: формальные методы и алгоритмы . Спрингер. п. 521. ИСБН 978-3-540-00296-3 .

[11] Систла, АП; Кларк, Э.М. (1 июля 1985 г.). «Сложность пропозициональной линейной темпоральной логики» . Дж. АКМ . 32 (3): 733–749. дои : 10.1145/3828.3837 . ISSN 0004-5411 .

[12] Варди, МЮ (1 января 1988 г.). «Исчисление временных фиксированных точек». Материалы 15-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '88 . Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 250–259. дои : 10.1145/73560.73582 . ISBN 0897912527 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]