モーダルμ計算

理論計算機科学では、様相μ計算（Lμ、Lμ _、または命題μ計算^{[ 1 ]}、時には単にμ計算と呼ばれるが、これはより一般的な意味を持つこともある）は、最小不動点演算子μと最大不動点演算子νを追加することによって命題様相論理（多くの様相を持つ）を拡張したものであり、したがって不動点論理である。

（命題論理、様相論理）μ計算は、Dana ScottとJaco de Bakker ^{[ 2 ]}によって始まり、Dexter Kozen ^{[ 3 ]}によって現在最もよく使われているバージョンへと発展しました。これは、ラベル付き遷移システムの特性を記述し、これらの特性を検証するために使用されます。CTL *とその広く使われている断片である線形時相論理と計算木論理^{[ 4 ]}など、多くの時相論理をμ計算に符号化することができます。

代数的な見方では、これを関数合成と最小および最大の不動点演算子からなる演算子を持つ完備束上の単調関数の代数と見なすことができる。この観点からすると、モーダルμ計算は冪集合代数の束上にある。^{[ 5 ]} μ計算のゲーム意味論は、完全情報を持つ2人ゲーム、特に無限パリティゲームに関連している。^{[ 6 ]}

P（命題）とA （行為）を2つの有限な記号集合とし、Varを可算無限個の変数集合とする。命題的、様相的μ計算の式の集合は次のように定義される。

• それぞれの命題とそれぞれの変数は、数式である。
• もし${\displaystyle \phi }$そして${\displaystyle \psi }$式である場合、${\displaystyle \phi \wedge \psi }$これは数式です。
• もし${\displaystyle \phi }$式である場合、${\displaystyle \neg \phi }$これは数式です。
• もし${\displaystyle \phi }$は公式であり、${\displaystyle a}$アクションの場合、${\displaystyle [a]\phi }$は公式です。（発音はどちらでも可：${\displaystyle a}$箱${\displaystyle \phi }$またはその後${\displaystyle a}$必然的に${\displaystyle \phi }$）
• もし${\displaystyle \phi }$は公式であり、${\displaystyle Z}$変数、${\displaystyle \nu Z.\phi }$は式であり、すべての自由な出現は${\displaystyle Z}$で${\displaystyle \phi }$肯定的に発生する、つまり偶数個の否定の範囲内で発生する。

（自由変数と束縛変数の概念は通常通りで、${\displaystyle \nu }$（唯一の束縛演算子です。）

上記の定義を踏まえると、構文を以下のように拡張することができます。

• ${\displaystyle \phi \lor \psi }$意味${\displaystyle \neg (\neg \phi \land \neg \psi )}$
• ${\displaystyle \langle a\rangle \phi }$（発音はどちらでも可：${\displaystyle a}$ダイヤモンド${\displaystyle \phi }$またはその後${\displaystyle a}$おそらく${\displaystyle \phi }$） 意味${\displaystyle \neg [a]\neg \phi }$
• ${\displaystyle \mu Z.\phi }$手段${\displaystyle \neg \nu Z.\neg \phi [Z:=\neg Z]}$、 どこ${\displaystyle \phi [Z:=\neg Z]}$置き換えることを意味する${\displaystyle \neg Z}$のために${\displaystyle Z}$すべての自由な出現において${\displaystyle Z}$で${\displaystyle \phi }$。

最初の 2 つの式は、それぞれ古典的な命題論理と最小多様体論理Kでおなじみのものです。

表記法${\displaystyle \mu Z.\phi }$（およびその双対）はラムダ計算から着想を得ており、その意図は式の最小（および最大）固定点を表すことである。${\displaystyle \phi }$ここで「最小化」（およびそれぞれ「最大化」）は変数で行われる${\displaystyle Z}$ラムダ計算とよく似ている${\displaystyle \lambda Z.\phi }$式を持つ関数です${\displaystyle \phi }$束縛変数内${\displaystyle Z}$; ^{[ 7 ]} 詳細については、以下の指示的意味論を参照してください。

（命題）μ計算のモデルは、ラベル付き遷移システムとして与えられる。${\displaystyle (S,R,V)}$どこ：

• ${\displaystyle S}$は状態の集合である。
• ${\displaystyle R}$各ラベルにマッピングされます${\displaystyle a}$二項関係${\displaystyle S}$;
• ${\displaystyle V:P\to 2^{S}}$各命題をマッピングします${\displaystyle p\in P}$その命題が真となる状態の集合へ。

ラベル付き遷移システムが与えられた場合${\displaystyle (S,R,V)}$そして解釈${\displaystyle i}$変数の${\displaystyle Z}$の${\displaystyle \mu }$-微積分、${\displaystyle [\![\cdot ]\!]_{i}:\phi \to 2^{S}}$は、以下の規則によって定義される関数です。

• ${\displaystyle [\![p]\!]_{i}=V(p)}$;
• ${\displaystyle [\![Z]\!]_{i}=i(Z)}$;
• ${\displaystyle [\![\phi \wedge \psi ]\!]_{i}=[\![\phi ]\!]_{i}\cap [\![\psi ]\!]_{i}}$;
• ${\displaystyle [\![\neg \phi ]\!]_{i}=S\smallsetminus [\![\phi ]\!]_{i}}$;
• ${\displaystyle [\![[a]\phi ]\!]_{i}=\{s\in S\mid \forall t\in S,(s,t)\in R_{a}\rightarrow t\in [\![\phi ]\!]_{i}\}}$;
• ${\displaystyle [\![\nu Z.\phi ]\!]_{i}=\bigcup \{T\subseteq S\mid T\subseteq [\![\phi ]\!]_{i[Z:=T]}\}}$、 どこ${\displaystyle i[Z:=T]}$地図${\displaystyle Z}$に${\displaystyle T}$マッピングを維持しながら${\displaystyle i}$その他の場所。

双対性によって、他の基本公式の解釈は次のようになる。

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

より非公式に言えば、これは、特定の遷移システムに対して、${\displaystyle (S,R,V)}$:

• ${\displaystyle p}$状態の集合内で保持する${\displaystyle V(p)}$;
• ${\displaystyle \phi \wedge \psi }$すべての州で${\displaystyle \phi }$そして${\displaystyle \psi }$両方とも有効です。
• ${\displaystyle \neg \phi }$すべての州で${\displaystyle \phi }$成り立たない。
• ${\displaystyle [a]\phi }$状態を保持する${\displaystyle s}$もしすべての${\displaystyle a}$-移行から${\displaystyle s}$次のような状態につながる${\displaystyle \phi }$保持する。
• ${\displaystyle \langle a\rangle \phi }$状態を保持する${\displaystyle s}$存在する場合${\displaystyle a}$-移行から${\displaystyle s}$それは次のような状態につながる${\displaystyle \phi }$保持する。
• ${\displaystyle \nu Z.\phi }$任意のセットの任意の状態を保持する${\displaystyle T}$変数が${\displaystyle Z}$設定されています${\displaystyle T}$、 それから${\displaystyle \phi }$すべてに適用される${\displaystyle T}$（クナスター・タルスキの定理から、${\displaystyle [\![\nu Z.\phi ]\!]_{i}}$最大の固定点は${\displaystyle T\mapsto [\![\phi ]\!]_{i[Z:=T]}}$、 そして${\displaystyle [\![\mu Z.\phi ]\!]_{i}}$その最小固定点。）

解釈${\displaystyle [a]\phi }$そして ${\displaystyle \langle a\rangle \phi }$これらは実際には動的論理の「古典的な」ものです。さらに、演算子${\displaystyle \mu }$生気（「いずれ何か良いことが起こる」）と解釈でき、${\displaystyle \nu }$レスリー・ランポートの非公式な分類では、安全性（「何も悪いことは起こらない」）として定義される。 ^{[ 8 ]}

様相μ計算式の充足可能性はEXPTIME完全である。^{[ 11 ]}線形時相論理と同様に、^{[ 12 ]}線形様相μ計算のモデル検査、充足可能性、妥当性の問題もPSPACE完全である。^{[ 13 ]}

実際、次数付きモーダルμ計算の充足可能性問題の複雑さもEXPTIME完全であり、モダリティの数値がバイナリで記述されていても同様である（次数付きモーダルμ計算は、「少なくともk個の後継者が存在し、…である」というモダリティを持つ標準モーダルμ計算の拡張である）。^{[ 14 ]}

様相論理は、標準的な変換によって一階述語論理（FO）に変換できることを思い出してください。${\displaystyle ST}$一次変数によってインデックス付けされる${\displaystyle x}$現在の状態を表す：

${\displaystyle {\begin{aligned}ST_{x}(p)&:=p(x)\\ST_{x}(\lnot \phi )&:=\lnot ST_{x}(\phi )\\ST_{x}(\phi \land \psi )&:=ST_{x}(\phi )\land ST_{y}(\psi )\\ST_{x}([a]\phi )&:=\forall y,xR_{a}y\rightarrow ST_{y}(\phi )\end{aligned}}}$

単項二階論理（MSO）は、部分集合に対する二階量化を用いて一階論理（FO）を拡張したものであることを思い出してください。標準的な変換はμ計算に拡張され、固定点演算子に以下の変換規則を追加することで単項二階論理に変換できます^{[ 15 ]}。

${\displaystyle {\begin{aligned}ST_{x}(\mu X.\phi )&:=\forall X,(\forall y,ST_{y}(\phi )\rightarrow y\in X)\rightarrow x\in X)\\ST_{x}(\nu X.\phi )&:=\exists X,(\forall y,y\in X\rightarrow ST_{y}(\phi ))\land x\in X)\end{aligned}}}$

JaninとWalukiewiczは1996年に、双同化によって不変なモナド2階の任意の式は、あるμ計算式と等価であることを証明した^{[ 1 ]}。

• 有限モデル理論
• 交替のないモーダルμ計算

• クラーク、エドモンド・M・ジュニア、オルナ・グランバーグ、ドロン・A・ペレド（1999）。モデル検査。米国マサチューセッツ州ケンブリッジ：MIT出版。ISBN 0-262-03270-8。第7章、μ計算のモデル検査、 97～108ページ
• スターリング、コリン。（2001）。プロセスの様相と時間的特性。ニューヨーク、ベルリン、ハイデルベルク：シュプリンガー・フェルラーク。ISBN 0-387-98717-7。、第 5 章、モーダルμ計算、pp.  103–128
• アンドレ・アーノルド。ダミアン・ニウィンスキー (2001)。μ微積分の初歩。エルゼビア。ISBN 978-0-444-50620-7。第6章「冪集合代数上のμ計算」（ 141～153ページ）は、様相μ計算についてです。
• イデ・ヴェネマ（2008）モーダルμ計算に関する講義；第18回ヨーロッパ論理・言語・情報サマースクールにて発表
• Bradfield, Julian & Stirling, Colin (2006). "Modal mu-calculi" . P. Blackburn、J. van Benthem、F. Wolter (編) 『The Handbook of Modal Logic』Elsevier、pp. 721–756。 
• エマーソン、E.アレン（ 1996 ）。「モデル検査とμ計算」。記述的複雑性と有限モデル。アメリカ数学会。pp. 185–214。ISBN  0-8218-0517-7。
• Kozen, Dexter (1983). 「命題μ計算に関する結果」. Theoretical Computer Science . 27 (3): 333– 354. doi : 10.1016/0304-3975(82)90125-6 .

• ソフィー・ピンチナット氏によるANUロジックサマースクール'09での講義のビデオ録画（論理、オートマタ、ゲーム）