Python でモデル検査

ちゅらデータの k.ueda です。[8日](https://qiita.com/kueda_cs/items/605eb56b0a7ad2703759)と[22日](https://qiita.com/kueda_cs/items/d41fd7839b07ac8d41bf)に引き続き、[ちゅらデータ Advent Calender](https://qiita.com/advent-calendar/2021/churadata) 3回目のエントリーです。23日目の記事では形式検証の話をします。

# モデル検査とは
　システム（ソフトウェア）が正常に動くかどうかを確かめることは重要です。意図しない動作があり得たり、意図した動作が実現しなかったりすると大変に困ります。踏切やエレベータにそのような誤作動の可能性があれば人命にもかかわります。モデル検査はそういったシステムがうまく動くかのチェックに利用される形式検証手法です。時相演算子 $\Box, \Diamond$ などを用いる非古典論理体系である線形時相論理（Linear Temporal Logic; LTL）や計算木論理（Computational Tree Logic; CTL）でシステムの性質を記述し、クリプキモデルと呼ばれる状態遷移系で表現されたシステムがそれを満たすかどうかを調べることがモデル検査の主な関心です。

## 様相論理とクリプキモデル
　まず、システム上で起こりうることの最小単位（これを原始命題で表現する）をあつめた集合 $\mathbf{AP}$ を用意します。命題論理では論理演算子として $\land, \lor, \lnot, \rightarrow$ を考え、原始命題とこれらの論理演算子を組み合わせてつくられたものを**命題論理式**とし、あらかじめ定められた推論規則に従って（構文論）。また、**付値**と呼ばれる関数 $V:\mathbf{AP} \rightarrow \left\\{\mathtt{True}, \mathtt{False}\right\\}$ によって原始命題およびそこから構成される命題論理式の真偽を考えました（意味論）。
　**様相論理**ではこれに**様相演算子** $\Box$ を加えます。可能世界について考えたい場合は「必ず」、義務について考えたい場合は「しなければならない」、知識について考えたい場合は「知っている」、等々を表すものとして利用されます。また、様相論理式 $\varphi$ に対して $\Diamond \varphi$ を $\lnot\Box\lnot\varphi$ の略記として利用することも多いです。「必ず」と対応して意味を考えるならば「かもしれない」と思えばよいでしょう。
　様相論理の意味論は**クリプキモデル** $K = \left(F, V \right)$ によって与えることができます。ここで、**クリプキフレーム** $F = \left(Q, \preceq\right)$ は**状態**または**可能世界**と呼ばれる要素を持つ集合 $Q\neq\emptyset$ と前順序 $\preceq$ の組であり、付値 $V: Q\times\mathbf{AP} \rightarrow \left\\{ \mathtt{True}, \mathtt{False}\right\\}$ は状態と原始命題を引数に持つ関数です。以後、前順序 $\preceq$ を二項関係 $R \subseteq Q \times Q$ とみなします。この $R$ を**到達可能関係**と呼びます。様相論理の意味論の与え方については[蓮尾一郎氏の講義資料](https://www.kurims.kyoto-u.ac.jp/~cs/lecture2009/lecture09ModelChecking.pdf)を参照してください。

## LTL と CTL
　**時相論理**は様相論理の一種で、様相演算子 $\Box$ を「これ以降常に」と捉えたものです。$\Diamond$ は「これ以降のいつかに」と思うことができます。時相論理の場合は様相演算子をそれぞれ $\mathsf{G}, \mathsf{F}$ と表記することもあります。また、「次の時点で」を表すために $\bigcirc$ または $\mathsf{X}$ という演算子を考えたりします。 時相論理には大きく分けて**線形時間時相論理**と**分岐時間時相論理**のふたつがあり、それぞれ LTL と CTL がよく知られています。前者では時間の経路が定まれば状態遷移は一通りに定まりますが、後者では時間を木構造で扱うので状態遷移が一通りとは限りません。
　LTL ではこれまでに考えた演算子に加えて $\mathsf{U}$ を考えます。$\varphi\ \mathsf{U}\ \psi$ で「$\psi$ となるまでの間は $\varphi$ であり続ける」ということを表します。英語の "until" そのままですね。$\varphi\ \mathsf{R}\ \psi \equiv \lnot\left(\lnot\varphi\ \mathsf{U}\ \lnot\psi\right)$ として演算子 $\mathsf{R}$ を追加することもあります。
　CTL ではさらに**パス限定子** $\mathsf{A}, \mathsf{E}$ を考えます。それぞれ「これ以降のすべての分岐で」「これ以降のある分岐で」という限定を表す演算子です。例えば $\mathsf{A}\Box\lnot\left(a \land b \right)$ という CTL 式は「$a$ と $b$ が同時に起こることはない」ということを意味します。

## モデル検査
　モデル検査ではクリプキモデル $K$ と時相論理式 $\varphi$ に対して $\varphi$　を満たす状態の集合 $Q\left(\varphi\right) = \left\\{ q \in Q\ \middle|\ K,q \models \varphi \right\\}$ を求めます。システム実行開始時の初期状態 $I$ が $I \subseteq Q\left(\varphi\right)$ となればこのシステムは性質 $\varphi$ を満たしてくれるということがわかります。

　モデル検査でよく考えられる性質として、以下のようなものが挙げられます。

- 安全性（safety）：望ましくないことは起こらない
- 活性（liveness）：望ましいことはいつか必ず起こる
- 到達可能性（reachability）：特定のことが起こる可能性がある
- 公平性（fairness）：特定のことが無限回実現する（任意の時刻においてどのタスクも有限時間内に実行される、等々）

　例えば、エレベータを制御するシステムであれば「ドアが開いたまま上昇・下降しない」という安全性や「緊急停止ボタンを押せば停止する」という活性を考えることが必要となりそうです。

# pyModelChecking を用いたモデル検査

　簡略化した踏切システムを考えましょう。

- 状態集合 $Q = \left\\{q_0, q_1, q_2  \right\\}$ 
- 遷移関係 $R = \left\\{\left(q_0, q_1\right), \left(q_0, q_2\right), \left(q_1, q_0\right), \left(q_2, q_0\right) \right\\}$
- 付値 $V = \left\\{\left(q_0, p, \mathtt{False}\right), \left(q_0, q, \mathtt{False}\right), \left(q_1, p, \mathtt{True}\right), \left(q_1, q, \mathtt{False}\right), \left(q_2, p, \mathtt{False}\right), \left(q_2, q, \mathtt{True}\right)  \right\\}$

としてクリプキモデル $K = \left(Q, R, V \right)$ で表されるようなシステムです。ここで、$p, q \in \mathbf{AP}$ はそれぞれ「電車が進入している」「遮断機が上がっている」という原始命題とします。ここまで簡略化すると明らかに変なことは起こらないとわかるのですが、とりあえずモデル検査してみます。状態 $q_0, q_1, q_2$ をそれぞれ「遮断機が下がっていて電車が進入していない」「遮断機が下がっていて電車が進入している」「遮断機が上がっていて電車が進入していない」ような状況を表すものとします。安全性・活性として「遮断機が上がっているのに電車が進入するようなことはない」「開かずの踏切ではない」という性質を考えます。すなわち、

- $\mathsf{A}\Box\lnot\left(p \land q \right)$
- $\mathsf{A}\Diamond q$

を初期状態たちが満たすかを調べます。`pyModelChecking` では状態集合、初期状態、遷移関係、付値をそれぞれ引数 `S`、`S0`、`R`、`L` に渡します。`S` は設定しなくとも `R` から読み取ってくれたりします。演算子 $\Box, \Diamond, \mathsf{A}, \lnot, \land$ はそれぞれ `G`、`F`、`A`、`Not`、`And` で表現します。

```Python
from pyModelChecking import Kripke
from pyModelChecking.CTL import And, Not, A, G, F, modelcheck

# 踏切システム
K_crossing = Kripke(
    S0=[0, 1, 2],
    R=[(0, 1), (0, 2), (1, 0), (2, 0)],
    L={0: [], 1: ['電車が進入している'], 2: ['遮断機が上がっている']})

# 安全性：遮断機が上がっているのに電車が進入するようなことはない
φ_safe = A(G(Not(And('電車が進入している', '遮断機が上がっている'))))
# 活性：開かずの踏切ではない
φ_live = A(F('遮断機が上がっている'))
```
　これらを満たす状態は

```Python
# 安全性を満たすか
modelcheck(K_crossing, φ_safe)
-> {0, 1, 2}

# 活性を満たすか
modelcheck(K_crossing, φ_live)
-> {2}
```
となっており、どの初期状態から始めても上記で定義した安全性は満たされます。開かずの踏切を回避するにはこれだけじゃダメみたいですね。例えば、 $$q_0 \rightarrow q_1 \rightarrow q_0 \rightarrow q_1 \rightarrow \cdots$$ となるような遷移が "反例" となります。以下のようなクリプキモデルで表現されるシステムではどうでしょう。

```Python
# 危険な踏切システム
K_crossing2 = Kripke(
    S0=[0, 1, 2],
    R=[(0, 1), (0, 2), (1, 0), (2, 0), (2, 3), (3, 1), (3, 2)],
    L={0: [], 1: ['電車が進入している'], 2: ['遮断機が上がっている'], 3: ['電車が進入している', '遮断機が上がっている']})
```
　これは電車が進入していてなおかつ遮断機が上がっているような状態への遷移を含むので、

```Python
# 安全性を満たすか
modelcheck(K_crossing2, φ_safe)
-> set()

# 活性を満たすか
modelcheck(K_crossing2, φ_live)
-> {2, 3}
```
というふうに初期状態 $q_0, q_1, q_2$ のどこから始めても安全でない状態に達してしまいます。

　`pyModelChecking` では他にも LTL や CTL*（LTL と CTL を組み合わせたもの）を扱うことができます。また、論理式を

```Python
from pyModelChecking.CTL import Parser

parser = Parser()
φ_safe = parser('A G not (p and q)')
```
のように文字列で渡すこともできます。日本語が入るとうまくパースしてくれないようです。

# 参考文献
- [蓮尾一郎. モデル検査入門. RIMS 講義資料, 2009.](https://www.kurims.kyoto-u.ac.jp/~cs/lecture2009/lecture09ModelChecking.pdf)
- [pyModelChecking's documentation](https://pymodelchecking.readthedocs.io/en/latest/index.html)