ちゅらデータの k.ueda です。8日と22日に引き続き、ちゅらデータ Advent Calender 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$ を到達可能関係と呼びます。様相論理の意味論の与え方については蓮尾一郎氏の講義資料を参照してください。
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 で表現します。
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('遮断機が上がっている'))
これらを満たす状態は
# 安全性を満たすか
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$$ となるような遷移が "反例" となります。以下のようなクリプキモデルで表現されるシステムではどうでしょう。
# 危険な踏切システム
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: ['電車が進入している', '遮断機が上がっている']})
これは電車が進入していてなおかつ遮断機が上がっているような状態への遷移を含むので、
# 安全性を満たすか
modelcheck(K_crossing2, φ_safe)
-> set()
# 活性を満たすか
modelcheck(K_crossing2, φ_live)
-> {2, 3}
というふうに初期状態 $q_0, q_1, q_2$ のどこから始めても安全でない状態に達してしまいます。
pyModelChecking では他にも LTL や CTL*（LTL と CTL を組み合わせたもの）を扱うことができます。また、論理式を
from pyModelChecking.CTL import Parser
parser = Parser()
φ_safe = parser('A G not (p and q)')
のように文字列で渡すこともできます。日本語が入るとうまくパースしてくれないようです。