ねこでも分かる 様相論理のお気持ち

ねこでも分かる 様相論理のお気持ち ゆにねこ

Q. 様相論理とは？

A. 様相を含む命題を扱う論理体系

「〜は必然的に真」や「〜は可能である」 といった必然性や可能性 A. 様相を含む命題を扱う論理体系 真偽 (True, False) が定まるもの

猫は必ず哺乳類である (□P, P: 猫は哺乳類) 半径 100m 以内に猫がいる可能性がある (◇Q, Q: 半径 100m 以内に猫がいる)

可能性は追加できた → 時間の概念を追加したい

Q. 時相論理とは？

A. 時間経過を追加した様相論理

状態遷移として表現 A. 時間経過を追加した様相論理

以降は CTL について話します CTL (Computation Tree Logic) … 時間経過を分岐と考える LTL (Linear Temporal Logic) … 時間経過を線形と考える

いつか必ず猫は死ぬ (AF) 明⽇は⾬が降る可能性がある (EX)

いつか必ず猫は死ぬ (AF) 明⽇は⾬が降る可能性がある (EX)

… … 誕⽣以降の任意のパスには Day1 誕⽣ Day1 Day1 … … Day2 … … いつか「☠」のノードが存在する (AF) … ☠ 死後 Day1 …

記号 (X, G, F, U) φ Xφ t₀ t₁ t₂ … Gφ t₀ t₁ t₂ … Fφ t₀ t₁ t₂ … tᵢ t₀ t₁ t₂ … tᵢ K, t₀ |= ψ ψUφ

記号 (A, E) … … t₀ t₁ t₂ … Eα α … t₀ t₁ … … … … Aα α … t₂ …

Q. 状態遷移に適⽤できるとなぜ嬉しいか？

A. 多くのシステムはステートマシンだから 特に組み込み

例1. 信号機 1 [sec] n [sec] Red m [sec] Green Yellow

例2. CPU https://www.cise.ufl.edu/~mssz/CompOrg/CDA-proc.html

• https://www.cise.ufl.edu/~mssz/CompOrg/CDA-proc.html

様相論理でテストコードを書きたい

NuSMV

NuSMV Dockerfile, compose.yaml (ゆにねこ作) New Symbolic Model Verifier 1. NuSMV をインストール 2. モデルを記述 (.smv) 3. 検証⽤の論理式を作成 4. 実⾏ https://gist.github.com/Harineko0/1e24d2cb8 a4e24c185cb5710a6fc073d

• https://gist.github.com/Harineko0/1e24d2cb8

デモ ソースコード https://gist.github.com/Harineko0/1967c8 5af32ed884e5ef5be8c1a8dc92

• https://gist.github.com/Harineko0/1967c8

参考⽂献, 引⽤

宣伝 https://gdsc-osaka-univ.connpass .com/event/350894/

• https://gdsc-osaka-univ.connpass