初めに
語らないこと
定理証明支援系を語らないため、自然演繹など証明を支援するための背景となる論理も語っていない。
語ること
CTL モデル検査ができるようになるための基本的な論理学的な背景を語ります。
参考文献
- 論理と計算のしくみ: https://www.iwanami.co.jp/book/b265606.html
- 命題論理・述語論理など形式論理の基礎を学んだあと，ゲーデル不完全性やラムダ計算について学習する．様相論理も語られているこれ一冊で事足りる超おすすめ。
古典論理
古典論理の意味論的射程は、排中律、真偽の二値（無矛盾律）で表現できる世界を対象としている。
アリストテレスの3つの思考の法則:
- 無矛盾律：ある事象について、同じ観点で、同時に、肯定しつつ、否定することはできない。
- 排中律
- 同一律
一階述語論理
では二階述語論理の論理式とは？
一階述語論理では、そのドメインの個々の元が変項の値となり、量化される。例えば、一階の論理式 ∀x (x ≠ x + 1) では、変項 x は任意の個体を表す。二階述語論理は個体の集合を変項の値とし、量化することができる。例えば、二階の論理式 ∀S ∀x (x ∈ S ∨ x ∉ S) は、個体の全ての集合 S と全ての個体 x について、x が S に属するか、あるいは属さないかのどちらかであるということを主張している。
二階述語論論理では、集合も量化することができると考えればよい。
発展
高階述語論理や型理論
ラッセルのパラドックスと型理論
ラッセルのパラドックス（英: Russell's paradox）とは、素朴集合論において、自身を要素として持たない集合全体からなる集合の存在を認めると矛盾が導かれるというパラドックス。
ラッセルの型理論（階型理論）の目的のひとつは、このパラドックスを解消することにあった[5]。
型付きラムダ計算
証明とは何か？自然演繹とはなにか？
https://ocw.kyoto-u.ac.jp/wp-content/uploads/2021/04/2010_tetsugakukisobunkaseminar-2_05.pdf
上記を考えるとカリーハワード同型対応の面白さがわかってくる。
カリーハワード同型対応
カリーハワード同型対応:
様相論理の導入としての可能世界
可能世界論（かのうせかいろん、英: possible world）は、論理学・哲学において、可能性、必然性、偶然性などの様相命題を論理的に扱うための理論的装置である。
量化だけでは表現できないような「様相」を表現するための論理として、可能世界論が生まれた。
例えば、「～ということが真であることも可能」だとか、いやいや「～ということは必然である」だとか言ったこと「様相」を表現することができれば「可能」な世界を表現できるようになる。
たとえば、以下のようなものである。
アル・ゴア副大統領は、大統領に当選した（といった事態が真であるような）可能性もある。
これは我々がどのような事態を「可能」だと、また我々の世界と同一の理論上で語れるかといった、哲学的な議論にもつながる。しかし、そういった哲学的な議論は置いておいて、こういった様相に関する論述を、論理学的な厳密性を与えたのが様相論理である。様相論理にはいくつかの表現力の異なる表現方法があるが、表現したいことに応じて理論体系を選択すればよい。
様相論理
古典論理の排中律が適応される世界だけでは、我々の認識にとって都合が悪いことがある。
- 宇宙人は存在するかもしれない。
- 宇宙人は存在しないはずだ。
後者は「今までの観測に基づくと」宇宙人らしきものは「存在を観測されていない」ことを示していると仮定すると、今後一切宇宙人が観測されることはない、ことをし否定しているとは解釈できない。
そこで、古典論理では表現できない、「～は可能である」「～は必然である」という意味論的な表現を、便利上、追加したものが様相論理である。
様相論理は、以下の二つの演算子を追加する。
- 必然性演算子：◻
- 可能性演算子: ◊
分配則
様相論理にも分配則は成立する。
P: 明日は雨だ
Q: 明日は寒い
と置いたとき、
◻(P∧Q) ⇒ ◻P ∧ ◻Q
直観的には以下のように解釈できる。
明日は雨で かつ 寒い ということは必然である(どこの世界でもそうだ)、
ならば、
明日はどこの雨であることは必然で、かつ、明日は寒いことも必然だ。
参照
- 時相論理とモデルチェッキング, 佐藤一郎, NII, https://research.nii.ac.jp/~ichiro/lecture/model2004/modal-logic.pdf
ドモルガン
様相論理でも、ド・モルガン的な関係が成立する。
意味論的には、以下のように解釈できる。
- 前者は「必然的にpは真」であるといっているので、「pが偽、である可能性は、ない」と同値といっている。
- 後者は「pは真であることが可能である」といっているので、「pが偽、であることが必然である、ことはない」とは同値だといっている。
ここに妥当だと思われる推論規則を足し合わせた公理系があり、その公理系に基づく検証を自動で行ってくれる便利なプログラムが形式手法的なプログラム検証で用いられる、とざっくりとらえてもらえればいいと思います。
参考
このような、古典論理だけでは表現できない日常的な、社会的な諸状態を追加しながら、論理的な厳密性を担保する考え方はほかにもある。
義務論理では、法律解釈などを厳密に行うことも可能だろう。この世の中の多くの社会人が論理学に精通していれば、契約や法律解釈のあいまいさを排除するために、すべて法律・契約概念を義務論理で記述して、諸問題、事態の解釈の正しさをコンピューターに問うことも可能になるだろう。
可能世界
ライプニッツから始まる、古典論理を拡張した世界の記述方法の一つ。哲学的な思惟、思索から始まり、クリプキらによって、論理学的に定式化されたと考えられる。
「可能世界」というくらいなので、いくつかの可能な世界があり、クリプキは（あいまいだが）中間的な「こんな事態もあり得るよね」という概念を認めるために、分岐した「可能な世界」を考えた。
- その中ですべての世界で成立する命題
- ある世界で成立し、ある世界では成立しない命題
- どの世界でも成立しない命題
参考文献
線形時相論理 LTL
ある状態が推移するような時間に関する様相を表現するために、時間表現を単純化した論理。
ある様相論理を表現するために、以下の作用素を追加したもの。
- N （next）
- G （globally）
- F （in the future）
- U （until）
- R （release）
計算木論理 CTL
未決定な複数の可能性が木の分岐のように残された未来を表現することができる論理。以下のような作用素を追加する。
- 経路作用素：
- A：分岐するすべての経路で～
- E: 分岐するある経路で～
- 状態作用素
- N: ある状態の次の状態では真
- G: ある状態の次以降のすべての経路で真
- F: ある状態の、いずれかの経路の状態では真（いつかは真）
- φ U ψ: ある時点でψが真になるまで、φは真。
- φ W ψ: ψが真になるまで、φは真。
このような表現ができることで、状態遷移を含む仕様の検証を行うことができる。例えば、
引用・参考：「モデル検査入門」, 蓮尾, https://www.kurims.kyoto-u.ac.jp/~cs/lecture2009/lecture09ModelChecking.pdf
導入
モデル検査
モデル検査とは？
SMVの文法
- ツールdl：https://nusmv.fbk.eu/
- 早水 公二（株式会社フォーマルテック）: https://codezine.jp/article/detail/10164
- モデル検査入門, https://www.jstage.jst.go.jp/article/sicejl/48/11/48_797/_pdf
練習問題
- 早水 公二（株式会社フォーマルテック), https://www.sci.kanagawa-u.ac.jp/info/kaiya/se/se09.pdf
時間制約つき時相論理
CTLは(時間の)経過とともに分岐する可能性のある状態遷移を表現できた。ここにさらに「～秒以内に必ず」などといった時間に関する表現をCTL（ComputationTreeLogic）の時相演算子に取り込んだのが、MTL（MetricTemporal Logic）と TCTL（Timed Computation Tree Logic）である。
(予告)UPPAL の紹介。
参考文献
参考: 形式手法のツール分類
- 「形式手法と仕様記述」の探求に向けて～形式手法とは？～, https://research.nii.ac.jp/~f-ishikawa/work/files/2012-05-11-SQiP-intro.pdf
参考：形式手法の必要性
ISO 26262では、OEMおよびサプライヤがそれぞれのデバイスを商用車（乗用車）に搭載して動作させるために従う必要のある機能安全開発プロセス（仕様定義から製品リリースまで）が規定されており、（準拠確認のために）そのプロセスを文書化する必要があります。この規格はリスク分類システム（Automotive Safety Integrity Level：ASIL）の概要を示し、「電気・電子（E/E）システムの機能不全のふるまいにより引き起こされるハザード」の可能性の低減を目指します。
ISO（International Organization for Standardization：国際標準化機構）はIEC（International Electrotechnical Commission：国際電気標準会議）と緊密に協働しています。ISO 26262仕様はE/Eシステムの汎用機能安全規格IEC 61508の改訂版として2011年に正式にリリースされました。
IEC61508（機能安全）では、
- Software safety requirements specification
- Software design and development : detailed design
において、安全度水準SIL2以上でFormal methodの適用が推奨されている。
参考文献
NuSVM
CTL
蓮尾先生のドキュメントは、CTLモデル検査のアルゴリズムが書かれている。