---
title: ねこでも分かる 様相論理のお気持ち
tags: 
author: [ゆにねこ](https://www.docswell.com/user/9031733)
site: [Docswell](https://www.docswell.com/)
thumbnail: https://bcdn.docswell.com/page/4JM2NVZ9JW.jpg?width=480
description: λ Kansai in Spring 2025 https://lambda-kansai.connpass.com/event/348567/  NuSMV Installation https://gist.github.com/Harineko0/1e24d2cb8a4e24c185cb5710a6fc073d  NuSMV Examples https://gist.github.com/Harineko0/1967c85af32ed884e5ef5be8c1a8dc92
published: April 12, 25
canonical: https://www.docswell.com/s/9031733/KQRQWE-2025-04-12-lambda-kansai-modal-logic
---
# Page. 1

![Page Image](https://bcdn.docswell.com/page/4JM2NVZ9JW.jpg)

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


# Page. 2

![Page Image](https://bcdn.docswell.com/page/PJRMD269E9.jpg)

Q. 様相論理とは？


# Page. 3

![Page Image](https://bcdn.docswell.com/page/PEXV1DM37X.jpg)

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


# Page. 4

![Page Image](https://bcdn.docswell.com/page/3EKQ2XGNED.jpg)

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


# Page. 5

![Page Image](https://bcdn.docswell.com/page/L73P45NZE5.jpg)

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


# Page. 6

![Page Image](https://bcdn.docswell.com/page/87DLQDW4EG.jpg)

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


# Page. 7

![Page Image](https://bcdn.docswell.com/page/VJP2LX9VJ8.jpg)

Q. 時相論理とは？


# Page. 8

![Page Image](https://bcdn.docswell.com/page/2EVDQLMREQ.jpg)

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


# Page. 9

![Page Image](https://bcdn.docswell.com/page/57GYWXG67L.jpg)

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


# Page. 10

![Page Image](https://bcdn.docswell.com/page/4EQM38X2JP.jpg)

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


# Page. 11

![Page Image](https://bcdn.docswell.com/page/KJ4V126PE1.jpg)

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


# Page. 12

![Page Image](https://bcdn.docswell.com/page/LE13GMVXJG.jpg)

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


# Page. 13

![Page Image](https://bcdn.docswell.com/page/GEWPK3LKJ2.jpg)

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


# Page. 14

![Page Image](https://bcdn.docswell.com/page/47ZKZVMN73.jpg)

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


# Page. 15

![Page Image](https://bcdn.docswell.com/page/YJ6QZ5N9JV.jpg)

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


# Page. 16

![Page Image](https://bcdn.docswell.com/page/GJ5RWY5D74.jpg)

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


# Page. 17

![Page Image](https://bcdn.docswell.com/page/LE3P455QJ5.jpg)

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


# Page. 18

![Page Image](https://bcdn.docswell.com/page/8EDLQDDWJG.jpg)

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


# Page. 19

![Page Image](https://bcdn.docswell.com/page/V7P2LXXX78.jpg)

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


# Page. 20

![Page Image](https://bcdn.docswell.com/page/2JVDQLL3JQ.jpg)

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


# Page. 21

![Page Image](https://bcdn.docswell.com/page/5EGYWXXYEL.jpg)

NuSMV


# Page. 22

![Page Image](https://bcdn.docswell.com/page/4JQM38867P.jpg)

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


# Page. 23

![Page Image](https://bcdn.docswell.com/page/K74V122MJ1.jpg)

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


# Page. 24

![Page Image](https://bcdn.docswell.com/page/LJ13GMMY7G.jpg)

参考⽂献, 引⽤


# Page. 25

![Page Image](https://bcdn.docswell.com/page/GJWPK33172.jpg)

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