様相μ計算
modal μ-calculus
時相論理
の中で最も表現力が高い論理
不動点演算子
を持つ
$ \begin{aligned}\varphi &::= P \mid \mathbf{X} \mid \neg \varphi \mid \varphi \vee \varphi \mid \Box \varphi \mid \mu X.\varphi\end{aligned}
$ \mu X.A
は
最小不動点
$ \nu X.\varphi[X] ::= \neg (\mu X. \neg \varphi[\neg X])
最大不動点
$ \nu
も使うらしい
/mrsekut-book-4007305803/132 ((d) 様相μ計算)