形式的手法のサーベイをおこなっていると、やはり不動点は避けて通れない。 前出のKripke構造のところであったが。まずは least fixedpoint: greatest fixedponit: というのが難問だなあ。どうしてになるものの下限（下のぎりぎり）が最小不動点になるかな？…

どうも "From PSL to NBA: a Modular Symbolic Encoding" によると。LTLはTableau法にてautomatonになるけども、PSLはLTLを拡張している からABA(Alternating Buchi Automata:universal and existential branchingが特徴)になるんだけども。 これをNBA(Non-d…

最近Kripke Structureにはまっている。原子命題AP上のKripke Structure Mとは４タプルである。 は有限の状態の集合 は初期状態の集合 は全象の遷移関係 は個々の状態で成立する命題の集合への写像関数 これは、Reactive Systemの基本モデル言語ともされるし…