Model Checking Ch.7

MC Ch.7: Automata on Infinite Words and LTL Model Checking #

  • Automata can describe system models and specifications.
  • MC can be done using automata.
  • LTL formulas are transformed to finite automata on infinite words.
  • Automaton-based MC is similar to that of tableau-based one:
    • Automaton-based : model and specification is described in automaton
    • Tableau-based : model and specification is described in tableau

Overview #

7.1: Finite Automata on Finite Words
Introduction of Automata.

7.2: Automata on Infinite Words
Introduction of Büchi Automata (automata over infinite words).

7.3: Deterministic versus Non-deterministic Büchi Automata
Discuss deterministic and non-deterministic of Büchi Automata.

7.4: Intersection of Büchi Automata
Discuss how to compute the intersection of two Büchi Automata.

7.5: Checking Emptiness
Discuss how to check emptiness of an automaton (Double DFS).
This technique is used in automata-based model checking.

7.6: Generalized Büchi Automata
Introduce fairness into the Büchi Automata.

7.7: Automata and Kripke Structures
Discuss how to transform a Kripke structure into an automaton.

7.8: Model Checking using Automata
Discuss how to use Double DFS to check whether a model specify a specification.

7.9: From LTL to Büchi Automata
Discuss how to transform LTL formulas into Büchi Automata (in naive way).

7.10: Efficient Translation of LTL into Automata

7.11: On-the-Fly Model Checking

7.1 Finite Automata on Finite Words #

A finite automaton over finite words \(\mathcal{A} \) is \((\Sigma, \mathcal{Q}, \Delta, \mathcal{Q}^0, F) \) s.t.

  • \( \Sigma \) is the finite alphabet
  • \( \mathcal{Q} \) is the finite set of states
  • \( \Delta \subseteq \mathcal{Q} \times \Sigma \times \mathcal{Q} \) is the transition relation
  • \( \mathcal{Q}^0 \subseteq \mathcal{Q} \) is the set of initial states
  • \( F \subseteq \mathcal{Q} \) is the set of accepting states

An automaton can be represented as a graph :

  • set of node : \( \mathcal{Q} \)
  • edges : given by \( \Delta \)

An example:

A finite automaton
  • \( \Sigma = \{a, b\} \)
  • \( \mathcal{Q} = \{q_1, q_2\} \)
  • \( \Delta = \{ \{q_1, a, q_1\}, \{q_1, b, q_2\}, \{q_2, b, q_2\}, \{q_2, a, q_1\}, \} \)
  • \( \mathcal{Q}^0 = \{q_1\} \)
  • \( F = \{q_1\} \)

\( v \) : a word in \( \Sigma ^{*} \) , length of \( |v| \)

  • run : A run of \( \mathcal{A} \) over \( v \) is a mapping \( \rho \) s.t.:
    • \( \rho : \{1,\ldots, |v| + 1\} \mapsto \mathcal{Q}\) s.t.:
      • \( \rho (1) \in \mathcal{Q}^0 \)
        • = First state is in the sets of initial states.
      • \( \mathrm{for} \, 1 \leq i \leq |v|, \, (\rho (i), v(i), \rho (i + 1)) \in \Delta \)
        • relation : \( \rho (i) \) – \( v \) –> \( \rho (i+1) \)
    • In the context of graph:
      • A run of \( \mathcal{A} \) over \( v \) : A path in automaton graph :
        • Path : \( \rho (0) \) –> \( \rho (|v| + 1) \)
        • Edges : labeled according to the letters in \( v \)
  • input : \( v \) is an input to the automaton.
  • accepting : A run \( \rho \) is accepting if \( \rho (|v| + 1) \in F\) .
    • (= if a run ends in one of accepting states)
  • accept : An automaton \( \mathcal{A} \) accepts a word \( v \) iff there is an accepting run of \( \mathcal{A} \) on \( v \) .
  • language : language of \( \mathcal{A} (=\mathcal{L}(\mathcal{A}) \subseteq \Sigma^{*})\) consists of all of words accepted by \( \mathcal{A} \)
Example
  • input : aabababaa (=$ v'$)
  • accept ? : yes because…
    • there is an accepting run ($q_1 q_1 q_1 q_2 q_1 q_2 q_1 q_2 q_1 q_1$)
  • language : $\varepsilon + (a + b)^{*}a$,
    • $+$ : or
    • $^*$ : repetition (including 0 times)

Types of automata

  • regular automata : finite automata over finite words
    • cf : regular language
  • $\omega$ -regular automata : finite automata over infinite words
    • cf : $\omega$-regular language

7.1.1 Determinization and Complementation #

Regular automata can be non-deterministic:

  • non-deterministic : there are transitions s.t. \( (q, a, l), (q, a, l') \in \Delta \, (l \neq l') \)
    • More than one transitions from a state labeled with the same alphabet.
  • deterministic : no such transitions and \( |\mathcal{Q}^0| = 1 \)

Determinization:

  • Subject : Non-deterministic finite automata over finite words
  • Property : Preserve the accepting language.
  • How to:
    • \(\mathcal{A} = (\Sigma, \mathcal{Q}, \Delta, \mathcal{Q}^0, F) \) : Non-deterministic automaton.
    • \(\mathcal{A'} = (\Sigma, \mathcal{P}(\mathcal{Q}), \Delta', \{\mathcal{Q}^0\}, F') \) : Deterministic automaton s.t.
      • \( \Delta' \subseteq \mathcal{P} (\mathcal{Q}) \times \Sigma \times \mathcal{P} (\mathcal{Q}) \) , where
        • \( (\mathcal{Q}_1, a, \mathcal{Q}_2) \in \Delta' \) if
          • \( \mathcal{Q}_2 = \bigcup_{q \in \mathcal{Q}_1} \{q' | (q, a, q') \in \Delta \} \)
      • \( F' = \bigcup_{\mathcal{Q}' \in \mathcal{P}(\mathcal{Q})} \{\mathcal{Q}' | \mathcal{Q}' \cap F \neq \empty\} \)
Example
Description

Complementation:

  • Subject : Finite automata over finite words
  • Property : Accept the language not accepted by the original one.
  • How to:
    • First, determinize if not yet.
    • Then, interchange the accepting states and the non-accepting state.
Example
Description

7.2 Automata on Infinite Words #

Finite automata over infinite words:

  • For reactive systems, which do not stop.
  • Same structure as finite automata over finite words.
  • Difference:
    • Language : Accepts words from $\Sigma^{\omega}$.
      • Thus, we should consider infinite run.

Abbreviation

  • FAFW : Finite Automata over Finite Words
  • FAIW : Finite Automata over Infinite Words

Büchi automata $\mathcal{A}$ (over infinite words $v$):

  • Simplest automata over infinite words.
  • Run $\rho$ : As same as that of FAFW:
    • But now words is infinite $|v| = \infty$.
  • Domain of run $\rho$ : $\mathbb{N}$ (set of all natural numbers)
  • Path : Also become infinite.

Acceptance of Büchi Automata:

  • $\mathit{inf}(\rho)$ : set of states that appear infinitely often in the run $\rho$.
  • $\mathit{inf}(\rho)$ is not empty because of the following:
    • Set of states $\mathcal{Q}$ is finite.
    • Run $\rho$ is infinite.
  • Acceptance condition:
    • $\mathit{inf} (\rho) \cap F \neq \empty$
      • Intuitively, some states from $F$ appear infinitely often.
Example

This can be interpreted as FAIW.

In the case of $(ab)^{\omega}$:

  • Run : $q_1 (q_1 q_2)^{\omega}$, which visits $q_1 \in F$ infinitely often.

Language:

  • $(b^{*}a)^{\omega}$
  • Infinitely many $a$’s.

7.3 Deterministic versus Non-deterministic Büchi Automata #

非決定的オートマトンの表現力

  • 表現力 : 決定的 Buchi オートマトン < 非決定的 Buchi オートマトン
  • このことを以下で証明する
lemma 7.1

$\mathcal{B}$ を決定的オートマトンとする。 全ての単語(word) $v \in \Sigma^{\omega}$ に対して

$v$ は $\mathcal{B}$ の言語
$\iff$ $\mathcal{B}$ が受理状態に到達するような “$v$ の prefix” が無限に多く存在する。

Proof

NOTE : 決定性より、初期状態からは 1 つのパスしか存在しないことに注意。

($\impliedby$):

  • (右辺)
    $\implies$ $v$ の prefix(es) によって無限回到達されるような $q \in F$ が少なくとも 1 つ存在する。
    • $\because$ $F$ は有限
  • If $v'$ and $v''$ are the finite prefixes of $v$ ($|v'| < |v''|$), then $v''$ extends $v'$
  • $v'$ と $v''$ が $v$ の有限長の prefix ($|v'| < |v''|$) とした時、$v''$ は $v'$ を伸ばしたものになる。($\because$ 決定性)
    • 下図を参照
  • すると、$v$ は $v'$, $v''$, … に一致するような一意に定まるパスとなる。
  • したがって、$v$ は受理される。

($\implies$):

  • (左辺)
    $\implies$ $q \in F$ に無限回到達するような実行 $v$ が存在する。
  • $q$ が出現するごとに $v$ の 有限長の prefix が取れる。

$\square$

lemma 7.2
非決定的 Buchi オートマトンは、決定的 Buchi オートマトンよりも表現力に優れる。
つまり、決定的 Buchi オートマトンで等価な言語を表せないような非決定的 Buchi オートマトンが存在する。
Proof

Confusing…

  • 証明の第一段落において、おそらく $a$ と $b$ が混同されている。

上のような Buchi オートマトン $\mathcal{B}$ を考える。
性質:

  • Alphabet : $\Sigma = \{a, b\}$
  • Language : $a$ が有限回のみ出現するような言語

上記の言語を認識する決定的なオートマトンは存在しない。 そのことを以下で証明する。

(背理法):

  • $\mathcal{C}$ は上記のような決定的なオートマトンと仮定する。
  • NOTE : For all finite word $\sigma$, $\sigma b^\omega \in \mathcal{L}(\mathcal{B})$ (not $\sigma a^{\omega}$)

Now let us find an infinite word which is accepted by both $\mathcal{C}$ and $\mathcal{B}$ (but not actually by $\mathcal{B}$).

  • 無限の単語列 $v_0$ $v_1$ $v_2$,… を以下のように作る:
    • $v_0 = \varepsilon$
    • $v_{i+1} = v_i a b^n$
      • $n$ : $v_{i+1}$ が $\mathcal{C}$ での受理状態に到達するような最小の整数
  • $v_i ab^\omega \in \mathcal{L} (\mathcal{B})$ ($\because$ NOTE above) なので、$v_{i+1}$ は存在する
  • ここで、$v_i$ は $v_{i+1}$ の prefix
  • 従って、全ての $v_i$ を prefix として含むような無限長の単語 $v$ が存在する
  • lemma 7.1 より、$\mathcal{C}$ は $v$ を受理する
  • しかし、$v$ は無限個の $a$ を含むため、$v \notin \mathcal{L}(\mathcal{B})$ だが、これは矛盾
    • つまり、
      1. $\mathcal{C}$ を、$\mathcal{L}(\mathcal{B})$ を受理するオートマトンと仮定
      2. Lemma 7.1 を使って、$\mathcal{C}$ によって受理される $v$ を構成
      3. $v$ は $\mathcal{B}$ でも受理されるべきだが、無限個の $a$ を含む
      4. この $v$ は $\mathcal{L}(\mathcal{B})$ に含まれないため、矛盾

$\square$

その他の性質

  • 上記の $\mathcal{L} (\mathcal{B})$ の補集合は決定的オートマトンで受理される。
    • つまり $a$ が無限回現れるような言語は決定的オートマトンで表現される
    • 下図参照
A finite automaton
lemma 7.3
The set of languages accepted by deterministic BA is not closed under complementation.

NOTE : Non-deterministic BA are closed under complementation.

7.4 Intersection of Büchi Automata #

2 つの Buchi オートマトンの積を計算する方法について見る。

2 つの Buchi オートマトンは以下:

$$ \mathcal{B}_1 = (\Sigma, \mathcal{Q}_1, \mathcal{Q}_1^0, \Delta_1, F_1) \\ \mathcal{B}_2 = (\Sigma, \mathcal{Q}_2, \mathcal{Q}_2^0, \Delta_2, F_2) $$

$\mathcal{L}(\mathcal{B_1})\cap\mathcal{L}(\mathcal{B_2})$ を受理する $\mathcal{B_1}\cap\mathcal{B_2}$ は以下:

$$ \mathcal{B_1} \cap \mathcal{B_2} = (\Sigma, \mathcal{Q}_1 \times \mathcal{Q}_2 \times \{0, 1, 2\}, \mathcal{Q}_1^0 \times \mathcal{Q}_2^0 \times \{0\}, \Delta, \mathcal{Q}_1 \times \mathcal{Q}_2 \times \{2\}) $$

遷移:

  • $((r_i, q_j, x), a, (r_m, q_n, y)) \in \Delta$ iff the following conditions hold:
    • $(r_i, a, r_m) \in \Delta_1$ かつ $(q_j, a, q_n) \in \Delta_2$
      • それぞれのオートマトンで $a$ でラベル付けされた遷移が存在する。
    • 状態の 3 つ目の要素に関して:
      • $x = 0$ かつ $r_m \in F_1 \implies y = 1$.
      • $x = 1$ かつ $q_n \in F_2 \implies y = 2$.
      • $x = 2 \implies y = 2$.
      • Otherwise, $y = x$.

その他は上のように定義。

可視化すると

Correctness:

  • $0 \longrightarrow 1$ : $r \in F_1$ が出現したら
  • $1 \longrightarrow 2$ : $q \in F_2$ が出現したら
  • 受理状態を $\mathcal{Q}_1 \times \mathcal{Q}_2 \times \{2\}$ とすることにより、
    $r \in F_1$ と $q \in F_2$ が無限回現れることが保証される。

Note:

  • 単純に $F$ を $F_1 \times F_2$ としてもうまくいかない:
    • $r \in F_1$ と $q \in F_2$ が同時に出現するのは有限回のみかもしれない。
      すなわち、個別には $r$ も $q$ も無限回出現する場合を受理できない。
Example

Intersection of the two BA above is:

(All nodes that cannot be reached is omitted.)

Question

Q: 以下の 2 つのオートマトンの積を求めよ

Description

A:

7.5 Checking Emptiness #

Buchi オートマトンが空であるかどうか (= 言語が空かどうか) を調べる方法を見る。

Lemma 7.4

以下を仮定する:

  • $\mathcal{B} = (\Sigma, \mathcal{Q}, \Delta, \mathcal{Q}^0, F)$
  • $\rho$ : accepting run of $\mathcal{B}$

以下の条件は同値である:

  1. $\mathcal{L} (\mathcal{B})$ が空でない
  2. $\mathcal{B}$ のグラフが以下のような SCC $C$ を含む
    • 受理状態を含む
    • $\mathcal{Q}^0$ (初期状態) から到達可能
  3. $\mathcal{B}$ のグラフが以下のパスを含む
    1. $q \in \mathcal{Q}^0 \rightarrow t \in F$
    2. $t \rightarrow t$ (loop back)
Logics of 1.$\iff$2.

1. $\iff$ 2.:

($\implies$):

  • 空でないならば、受理される実行 $\rho$ が存在する。
  • $\rho$ は $F$ に含まれる状態を無限に含む
    • $\because$ “受理” の定義
  • $\mathcal{Q}$ は有限である
    $\implies$ $\rho$ の suffix で、その上の状態が無限に現れるような suffix $\rho'$ が存在する。
    • つまり、$\rho'$ によって無限回到達されるような状態が存在する
  • $\implies$ $\forall s, s' \in \rho$, $s$ は $s'$ から到達可能(逆も然り)
    • (つまり、$s \leftrightarrows s'$)
  • $\implies$ $\rho'$ 上の状態は、グラフ $(\mathcal{Q}, \Delta)$ のトリビアルではない SCC に含まれる
    • これは $\mathcal{Q}^0$ から到達可能で、
    • 受理状態を含む

($\impliedby$):

  • 上記のような SCC は $\mathcal{B}$ で受理される実行を生成可能
Logics of 2.$\iff$3.

2. $\iff$ 3.:

($\impliedby$):

  • このようなサイクル中のノードは何らかの SCC に含まれる
    • このようなサイクル: $t \rightarrow t$ (loop back)

($\implies$):

  • 受理状態を含む SCC が渡されたら、受理状態を通るサイクルを常に構成可能

結果:

  • Buchi オートマトンが空かどうかは、SCC $C$ を見つけることによって分かる
  • $\mathcal{L}(\mathcal{B})$ が空でない $\iff$ 到達可能で、自身へ戻るサイクルを持つ $q \in F$ が存在する
    • $\because$ 1. $\iff$ 3. in Lemma 7.4.

空に対する反例:

  • 有限世界で反例を表現可能
  • 形式: prefix + repetition
    • e.g. $12(32)^\omega$
Example of lemma 7.4

lemma 7.4 中の 3 つの同値な条件は以下:

  1. $\mathcal{L}(\mathcal{B_1} \cap \mathcal{B_2})$ が空でない。
  2. $\mathcal{B_1} \cap \mathcal{B_2}$ contains SCC $\{2, 3, 4, 5\}$
    • 初期状態 $1$ から到達可能
    • 受理状態 $3$ を含む
  3. $\mathcal{B_1} \cap \mathcal{B_2}$ は以下のパスを含む:
    1. $q \in \mathcal{Q}^0 \rightarrow t \in F$ : $1 \rightarrow 2 \rightarrow 3$
    2. $t \rightarrow t$ (loop back) : $3 \rightarrow 4 \rightarrow 2 \rightarrow 3$

空に対する反例 (の 1 つ):

  • $12(342)^\omega$
Qeustion
Q1: 受理状態を含み到達可能なSCCを 1 つ見つけよ
  • $\{3, 5, 2\}$, $\{3, 5, 4, 2\}$, …
Q2: 空に対する反例を 1 つ見つけよ

Double DFS アルゴリズムは 3 つ目の条件に依拠する。

7.5.1 Checking Emptiness with Double DFS #

DoubleDFS:

  • Buchi オートマトンが空かどうか判定できる。
  • SCC の発見とその解析を同時に行う。
    • 別々に見るより効率的。
    • 特に、On-the-Fly MC で役に立つ
  • $q \in \mathcal{F}$ から $q$へのサイクルを発見する。

2 つの DFS algorithms はインターリーブしている:

  • 1 つ目の DFS の途中で 2 つ目の DFS が開始される。
    • 2 つ目の DFS が終了->1 つ目 or 全体が終了

Double DFS works の具体例を確認:

Example of Double DFS

Two DFS:

  • DFS1 : 到達可能な受理状態を見つける。
  • DFS2 : サイクルを見つける。
01
02
03
04
05

$2$ and $5$ は DFS1 によって到達済み。 戻る。

06
07
08

$2$ and $5$ は DFS1 によって到達済み。 戻る。

09

DFS2 は $3$ から始まる。なぜなら:

  • $3$ 以降のノードが全て到達済み
  • $3$ は受理状態
10
11

$2$ は DFS1 のスタックにある。DFS2 はここで終了する。

結果:

  • prefix : $(1, 2, 3)$
    • DFS1 のスタック上にある
  • cycle : $(5, 2, 3)$
    • DFS1 と DFS2 のスタック上にある
  • 空に対する反例:
    • $123(523)^\omega$
Algorithm (in Python-like manner)

注意:

  • hashed : DFS1 によって訪問された時
  • flagged : DFS2 によって訪問された時
1def emptiness():
2    q: Node
3    Q_0: set[Node]  # set of initial states
4
5    for q in Q_0:
6        dfs1(q)
7    terminate(false)

 1def dfs1(q: Node):
 2    q_suc: Node
 3
 4    hash(q)
 5    for q_suc in successor(q):
 6        if not hashed(q_suc):
 7            dfs1(q_suc)
 8
 9        if is_accepting(q):
10            dfs2(q)

 1def dfs2(q: Node):
 2    q_suc: Node
 3
 4    flag(q)
 5    for q_suc in successor(q):
 6        if on_dfs1_stack(q_suc):
 7            terminate(true)  # <- found a cycle
 8
 9        else if not flaged(q_suc):
10            dfs2(q_suc)

7.5.2 Correctness of the Double DFS Algorithm #

Lemma 7.7

$q$をどのサイクルにも属さないノードとする。 DFS のアルゴリズムが$q$をバックトラックするのは、$q$から到達可能な全てのノードを探索し(かつ、バックトラックし)終わった場合のみ。

※$q$をバックトラックする = DFS のスタックから$q$が pop される

Theorem 7.8
$\mathcal{L}(\mathcal{B})$が空でない
$\iff$ DoubleDFS アルゴリズムは、オートマトン$\mathcal{B}$の空に対する反例を返す
Proof

($\impliedby$):

  • 反例があるので明らか。

($\implies$):

対偶:
「DoubleDFS アルゴリズムは、オートマトン$\mathcal{B}$の空に対する反例を返さない $\implies$ $\mathcal{L}(\mathcal{B})$は空」

以下の状況を仮定する(下図を参照)。

image of double dfs

サイクルが存在する場合、以下の 2 通りの出力がある：

  1. $q$から、DFS1 の探索 stack 上にある状態への(unflagged な(=DFS2 で訪問されていない)状態のみで構成される)パスが存在する。
    → この場合、$q$を通るサイクルを正しく発見する。
  2. $q$から、DFS1 の探索 stack 上にある状態へのパスの全てにおいて、途中に flagged な(DFS2 で訪問済みの)状態$r$がある。
    → この場合、$q$を通るサイクルを発見しない。

2 つ目の場合が無いことを背理法を用いて証明する。

すなわち、上のような状態$r$が存在すると仮定する。

状態$q, r, q'$をそれぞれ次のような状態とする：

  • $q$ : 受理状態。$q$を含むサイクルが存在するが、DFS2 がサイクルの発見に失敗するような最初の状態。
  • $r$ : $q$から始まる DFS2 で訪問される状態のうち、flagged な状態(= 別の DFS2 によって訪問済みの状態)でかつ、一番最初に訪問される状態。
  • $q'$ : 受理状態で、$r$を一番最初に訪問した DFS2 が始まった状態。

$q$から DFS2 が始まる直前を考える。状態$r$のパターンは 2 通りある：

  • (2a)$q'$が$q$から到達可能な場合
  • (2b)$q'$が$q$から到達不可能な場合

2a. $q'$が$q$から到達可能な場合：

figure0706a
  • サイクルが存在
    • $q' \rightarrow \dots \rightarrow r \rightarrow \dots \rightarrow p \rightarrow \dots \rightarrow q \rightarrow \dots \rightarrow q'$
    • 図の通り
  • このサイクルは$q'$から始まる DFS2 で見つかっていないはず
    • 見つかっていたらその時点でアルゴリズムが終了するから
  • これは、$q$がサイクルの発見に失敗する最初の状態であることに矛盾

2b. $q'$が$q$から到達不可能な場合：

figure0706b
  • $q'$はサイクルに含まれない
    • 含まれる場合、$q$がサイクルの発見に失敗する最初の状態であることに矛盾
      • 上と同じ
  • $q'$から$q$は到達可能
    • 図より、$q' \rightarrow \dots \rightarrow r \rightarrow \dots \rightarrow q$のパスが存在
  • DFS1 の探索は$q'$より$q$の方が早く行われる
    • より正確には、"$q$の発見及びそこからのバックトラックは$q'$より早い"
    • lemma 7.7 より
      • lemma 7.7 : とある状態からの DFS のバックトラックは、そこから到達可能な全ての状態を探索しバックトラックした時かつその時に限り行われる。
  • 以上より、DFS2 は$q'$よりも先に$q$から行われる。
  • これは、DFS2 の開始順序の仮定に矛盾する。
    • より細かくいうと、$q$からの DFS2 が開始される時点で$q'$からの DFS2 が$r$を訪問していることに矛盾

以上より、上記の 2 の場合はない。 従って、以下の対偶は真。

対偶:
「DoubleDFS アルゴリズムは、オートマトン$\mathcal{B}$の空に対する反例を返さない $\implies$ $\mathcal{L}(\mathcal{B})$は空」

以上より証明された。 $\square$

7.6 Generalized Büchi Automata #

特徴:

  • 受理状態集合を複数もつ
  • (Non-generalized な場合と比べて)受理できる言語の集合を拡張するわけでは無い
  • クリプキ構造における複数の公平性制約や、ここでの受理状態集合に相当する

モチベーション:

  • LTL 式で表現された仕様を generalized Buchi Automata に変換する方法がある

Generalized Buchi Automaton:

  • 受理状態に表現する$F$を次のように変更する : $F \subseteq \mathcal{Q} \rightarrow F \subseteq \mathcal{P}(\mathcal{Q})$
    • つまり、$F = \{ P_1, \dots, P_2 \}$. ただし、$P_i \subseteq Q (1 \leq i \leq k)$
  • 実行$\rho$は以下の場合に受理される
    • 全ての$P_i \in F$に対し、$inf(\rho) \cap P_i \neq \empty$

Generalized Buchi Automaton から Buchi Automaton への変換 #

Generalized Buchi Automaton $\mathcal{B}$ を以下のようにする:

  • $\mathcal{B} = (\Sigma, \mathcal{Q}, \mathcal{Q}', \Delta, F)$
    • ただし $F = \{ P_1, \dots, P_k \}$

以下の通常の Buchi Automaton を作る:

$$B' = (\Sigma , \mathcal{Q} \times \{0, \dots, k\}, \mathcal{Q}^0 \times \{0\}, \Delta ' ,\mathcal{Q} \times \{k\})$$

遷移関係$\Delta'$は以下のように定義する:

  • $((q, x), a, (q' ,y)) \in \Delta '$
    • $(q, a, q') \in \Delta$
    • かつ、$x, y$ が以下のルールで決められている時
      • $q' \in P_i$ かつ $x = i$ ならば $y = i + 1$
      • $x = k$ ならば $y = 0$
      • それ以外の場合は $y = x$

遷移関係の直感的な説明:

  • $(q, i)$ を訪問 ： $P_1, \dots ,P_i$ のそれぞれに含まれる状態を訪問済み
    • $(q, k)$ を訪問 ： $P_1, \dots ,P_k$ のそれぞれに含まれる状態を訪問済み

その他コメント #

  • 上記の変換はオートマトンのサイズを $k + 1$ 倍にする

7.7 Automata and Kripke Structures #

オートマトンを扱う利点：調べたい性質とシステムの両方が同じオートマトンで表せること。

ここでは、すでに見てきたクリプキ構造からオートマトンへの変換を考える。

変換方法 #

変換方法:

  • クリプキ構造 $M = (S, S_0, R, AP, L)$ は
    オートマトン $\mathcal{A}_M(\Sigma, S \cup \{\iota\}, \{\iota\}, \Delta, S \cup \{\iota\})$ に変換される
  • ただし:
    • アルファベット : $\Sigma = \mathcal{P}(AP)$
    • 遷移関係
      • $(s, a, s') \in \Delta \quad \mathrm{for} \quad s,s' \in S$ iff
        • $(s, s') \in R$ かつ $\alpha = L(s')$
      • さらに追加で、$(\iota, \alpha, s) \in \Delta$ iff
        • $s \in S_0$ かつ $\alpha = L(s)$
    • 受理状態集合
      • クリプキ構造 $M$ に公平性制約 $F$ が:
        • ない場合 : 全ての状態が受理状態
        • ある場合 : $F$ がそのまま受理状態集合
Figure 7.7

具体例:

figure0707

直感的な説明:

  • Kripke Structure での状態を、オートマトンでのその状態に入るエッジのラベルに変換
  • オートマトンでは、全ての状態が受理状態
    • これは、公平性制約が無いクリプキ構造での全てのパスは公平であることに対応。
  • 新たに状態 $\iota$ を追加
    • これはクリプキ構造での初期状態に相当

7.8 Model Checking using Automata #

  • システムをオートマトンで表現した
    → 調べたい性質もオートマトンで表現するのが自然。

システムの性質をオートマトンで表現する #

以下のそれぞれをオートマトンで表現する：

  • 相互排他(mutual exclusion) (fig 7.8)
  • eventuality property (fig 7.9)
fig0708

fig 7.8(left), fig 7.9(right)

エッジが boolean 表現で書かれている：

  • boolean 表現を true にするような AP の組み合わせ全てを含む遷移
    • e.g. $AP = \{X, Y, Z\}$, $X \land \lnot Y$ でラベル付けされているエッジは
      $\{X, Z\}$ と $\{X\}$ とラベル付けされたエッジに対応

fig 7.8：

  • 相互排他の性質を表す
    • “2 つのプロセスが同時にクリティカルセクションに入らない”
  • LTL 式 : $\mathbf{G}\lnot (CR_0 \land CR_1)$

fig 7.9：

  • “いつかは必ずクリティカルセクションに入る"を表す。
  • LTL 式 : $\mathbf{F} CR_0$

オートマトンを使ったモデル検証(概略) #

システムと調べたい性質がオートマトンで表現されているとする。

システム$\mathcal{A}$は以下の時にシステム$\mathcal{S}$を満たす：

$$\mathcal{L}(\mathcal{A}) \subseteq \mathcal{L}(\mathcal{S})$$

$\overline{\mathcal{L}(S)}$ を $\Sigma^\omega - \mathcal{L}(\mathcal{S})$ とすると

$$\mathcal{L}(\mathcal{A}) \cap \overline{\mathcal{L}(\mathcal{S})} = \emptyset$$

と書ける。

直感的な意味は、“システムの挙動の内、性質$\mathcal{S}$に禁止された挙動はない”。 空でなかった場合、反例が見つかる。

オートマトンを使ったモデル検証(具体的な手順) #

(システム : $\mathcal{A}$ 、調べたい性質 : $\mathcal{S}$ )

  1. $\mathcal{S}$ を反転させ、$\overline{\mathcal{S}}$ を得る
    • $\overline{\mathcal{L}(\mathcal{S})}$ を使いたいため
  2. $\mathcal{A}$ と $\overline{\mathcal{S}}$ の intersection を取る
  3. intersection 後のオートマトンが空かどうかチェックする
    • Double DFS アルゴリズムが使える
  4. 空だったら : 性質 $\mathcal{S}$ を満たす
    空じゃなかったら : 性質 $\mathcal{S}$ に対する反例が見つかる
Question

オートマトンで表されたシステム $\mathcal{A}$ が仕様 ($\mathbf{F}a$) を満たすかどうか調べたい。
システムのオートマトン $\mathcal{A}$ 、及び仕様のオートマトン $\mathcal{S}$ は以下のようになる。

Description

上記のシステムは仕様を満たすかどうか調べよ。

Answer

その他コメント #

  • Buchi Automaton の補集合を求める計算コスト : 大
    → 人間があらかじめ $\overline{\mathcal{S}}$ を与える戦略もある → (補集合を求めるのが簡単な) $\omega$-regular automaton を使う戦略もある
  • 次章以降では LTL 式 $\varphi$ を オートマトンに変換する方法を見る
    → $\lnot \varphi$ をオートマトンに変換すると、直接 $\overline{\mathcal{S}}$ が得られる

7.9 From LTL to Büchi Automata #

7.9, 7.10 では、LTL 式を (Generalized) Buchi Automaton に変換する手法を見る。 7.9 ではナイーブな方法を、7.10 ではより洗練された方法を見る。

LTL path 式を$\varphi$とする。

closure について

  • この closure 集合の部分集合を、最終的なオートマトンの状態としたい。
  • どんな部分集合かは good 条件を参照

$\varphi$ の closure ($cl(\varphi)$ と書く):

  • $\varphi$ のサブ式 (subformulas) とその否定 (negation) の集合
  • 形式的には、以下を満たす最小限の集合
    • $\varphi \in cl(\varphi)$
    • $\text{if} \; \varphi_1 \in cl(\varphi), \;\text{then}\; \lnot \varphi_1 \in cl(\varphi)$
    • $\text{if} \; \lnot\varphi_1 \in cl(\varphi), \;\text{then}\; \varphi_1 \in cl(\varphi)$
    • $\text{if} \; \varphi_1 \lor \varphi_2 \in cl(\varphi), \;\text{then}\; \varphi_1 \in cl(\varphi) \;\text{and}\; \varphi_2 \in cl(\varphi)$
    • $\text{if} \; \textbf{X}\varphi_1 \in cl(\varphi), \;\text{then}\; \varphi_1 \in cl(\varphi)$
    • $\text{if} \; \varphi_1\textbf{U}\varphi_2 \in cl(\varphi), \;\text{then}\; \varphi_1 \in cl(\varphi)\;\text{and}\; \varphi_2 \in cl(\varphi)$
Example

$cl(\lnot p\mathbf{U} ((\mathbf{X}q)\lor r)) = \{\lnot p\mathbf{U} ((\mathbf{X}q)\lor r), \lnot (\lnot p\mathbf{U} ((\mathbf{X}q)\lor r)), p, \lnot p,(\mathbf{X}q)\lor r, \lnot ((\mathbf{X}q)\lor r), \mathbf{X}q, \lnot (\mathbf{X}q), r, \lnot r, q, \lnot q \}$

教科書 p99 の例で $\{q, \lnot q\}$ が抜けている。

Q-closure

次の LTL path formula の closure を求めよ。

  • $\mathbf{X}((\lnot p\mathbf{U} q) \lor \lnot r)$
Answer
  • $cl(\mathbf{X}((\lnot p\mathbf{U} q) \lor \lnot r))$
    $= \{\mathbf{X}((\lnot p\mathbf{U} q) \lor \lnot r), \lnot (\mathbf{X}((\lnot p\mathbf{U} q) \lor \lnot r)),(\lnot p\mathbf{U} q) \lor \lnot r, \lnot ((\lnot p\mathbf{U} q) \lor \lnot r), \lnot p\mathbf{U} q, \lnot (\lnot p\mathbf{U} q), r, \lnot r, p, \lnot p, q, \lnot q\}$

good 条件

  • closure の部分集合をオートマトンの状態として扱う
    • その状態から始まる path で満たされる式を状態とする
  • 矛盾する状態は作らない
    • e.g. $p \land \lnot p$
    • このような式が含まれないことをgoodと言う

$S \subseteq cl(\varphi)$ は、以下の条件を満たす$cl({\varphi})$の最大の部分集合の時 good :

  • 全ての $\varphi_1 \in cl(\varphi)$ に対して、$\varphi_1 \in S \iff \lnot \varphi_1 \notin S$
  • 全ての $\varphi_1 \lor \varphi_2 \in cl(\varphi)$ に対して、
    $\varphi_1 \lor \varphi_2 \in S \iff \varphi_1$ か $\varphi_2$ のうち少なくとも一方が $cl(\varphi)$ に含まれる

オートマトンの構成

Atomic proposition の集合 $AP$ 上での LTL パス式 を $\varphi$ とする。
以下のオートマトン $\mathcal{A}_\varphi = (\mathcal{P}(AP), Q, Q^0, \Delta, F)$ に変換できる :

  • $\mathcal{Q} \subseteq \mathcal{P}(cl(\varphi))$ は $cl(\varphi)$ の内の全ての good 集合
  • 遷移は以下のように作る
    • $q, q'$ を状態とし、$\sigma \subseteq AP$ を文字とする。以下の条件が満たされる時 $(q, \sigma, q') \in \Delta$
      1. $\sigma = q \cap AP$
      2. 全ての $\mathbf{X}\varphi_1 \in cl(\varphi)$ に対して、$\mathbf{X}\varphi_1 \in q \iff \varphi_1 \in q'$
      3. 全ての $\varphi_1 \mathbf{U} \varphi_2 \in cl(\varphi)$ に対して、$\varphi_1 \mathbf{U} \varphi_2 \in q \iff \varphi_2 \in q \;\mathrm{or}\; (\varphi_1 \in q \;\mathrm{and}\; \varphi_1 \mathbf{U} \varphi_2 \in q')$
        • すなわち、全ての $\lnot(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対して、$\lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \iff \lnot\varphi_2 \in q \;\mathrm{and}\; (\lnot \varphi_1 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q')$
  • 初期状態 $Q^0 \subseteq Q$ は、$q \in Q$ の内 $\varphi \in q$ であるもの
  • 公平性制約 $F$ は次のように定める
    • $F$ は、全ての $(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対する
      集合 $P_{\varphi_1 \mathbf{U} \varphi_2} = \{ q \in Q | \varphi_2 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \}$ を全て含む
    • $F = \{\{\cdots\}, \{\cdots\},\cdots\}$
Example 7.10

LTL パス式 $\varphi = (\lnot h) \mathbf{U} c$ をオートマトンに変換する。
上記 LTL 式の closure $cl((\lnot h) \mathbf{U} c)$ は以下。

$$cl((\lnot h) \mathbf{U} c) = \{(\lnot h) \mathbf{U} c, \lnot((\lnot h) \mathbf{U} c), h, \lnot h, c, \lnot c\}$$

Closure の部分集合で good 条件を満たすものがオートマトンの状態 $\mathcal{Q}$ となる。

Closure と good 条件を考え、オートマトンの各状態は上記のようになる。

各状態のうち、$\varphi = (\lnot h) \mathbf{U} c$ を含む状態が初期状態。

  1. 全ての $\varphi_1 \mathbf{U} \varphi_2 \in cl(\varphi)$ に対して、$\varphi_1 \mathbf{U} \varphi_2 \in q \iff \varphi_2 \in q \;\mathrm{or}\; (\varphi_1 \in q \;\mathrm{and}\; \varphi_1 \mathbf{U} \varphi_2 \in q')$
  1. 全ての $\varphi_1 \mathbf{U} \varphi_2 \in cl(\varphi)$ に対して、
    $\varphi_1 \mathbf{U} \varphi_2 \in q \iff \varphi_2 \in q \;\mathrm{or}\; (\varphi_1 \in q \;\mathrm{and}\; \varphi_1 \mathbf{U} \varphi_2 \in q')$
  • $\varphi_2 = c$ が $1 (=q)$ が含まれるので、右辺は常に成立
  • よって、全ての状態に辺が張られる
  • $1$ と同様
  1. 全ての $\varphi_1 \mathbf{U} \varphi_2 \in cl(\varphi)$ に対して、
    $\varphi_1 \mathbf{U} \varphi_2 \in q \iff \varphi_2 \in q \;\mathrm{or}\; (\varphi_1 \in q \;\mathrm{and}\; \varphi_1 \mathbf{U} \varphi_2 \in q')$
  • $\varphi_1 = (\lnot h)$ が $3 (=q)$ に含まれる
  • $(\lnot h) \mathbf{U} c$ を含む状態に辺が張られる
  1. 全ての $\varphi_1 \mathbf{U} \varphi_2 \in cl(\varphi)$ に対して、
    $\varphi_1 \mathbf{U} \varphi_2 \in q \iff \varphi_2 \in q \;\mathrm{or}\; (\varphi_1 \in q \;\mathrm{and}\; \varphi_1 \mathbf{U} \varphi_2 \in q')$
  2. 全ての $\lnot(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対して、
    $\lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \iff \lnot\varphi_2 \in q \;\mathrm{and}\; (\lnot \varphi_1 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q')$
  • $\varphi_2 = c$ 及び $\varphi_1 = \lnot h$ が $4(=q)$ に含まれない
  • $4$ から張られる辺は存在しない
  • 全ての $\lnot(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対して、
    $\lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \iff \lnot\varphi_2 \in q \;\mathrm{and}\; (\lnot \varphi_1 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q')$
  • $\lnot \varphi_2 = \lnot c$ 及び $\lnot \varphi_1 = h$ が $5(=q)$ に含まれる
  • $5$ から全ての状態に辺が張られる
  • 全ての $\lnot(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対して、
    $\lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \iff \lnot\varphi_2 \in q \;\mathrm{and}\; (\lnot \varphi_1 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q')$
  • $\lnot \varphi_2 = \lnot c$ が $6(=q)$ に含まれない
  • $6$ からは辺が張られない
  • 全ての $\lnot(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対して、
    $\lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \iff \lnot\varphi_2 \in q \;\mathrm{and}\; (\lnot \varphi_1 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q')$
  • $\lnot\varphi_2 = \lnot c$ が $7(=q)$ に含まれる
  • $\lnot\varphi_1 = h$ が $7(=q)$ に含まれない
  • $\lnot ((\lnot h) \mathbf{U} c)$ が含まれる状態に辺が張られる
  • 全ての $\lnot(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対して、
    $\lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \iff \lnot\varphi_2 \in q \;\mathrm{and}\; (\lnot \varphi_1 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q')$
  • $\lnot\varphi_2 = \lnot c$ が $8(=q)$ に含まれない
  • $8$ からは辺が張られない

全てをまとめると、$(\lnot h) \mathbf{U}c$ は上記のオートマトンに変換できる。

公平性制約は以下より

  • 公平性制約 $F$ は次のように定める
    • $F$ は、全ての $(\varphi_1 \mathbf{U} \varphi_2) \in cl(\varphi)$ に対する
      集合 $P_{\varphi_1 \mathbf{U} \varphi_2} = \{ q \in Q | \varphi_2 \in q \;\mathrm{or}\; \lnot (\varphi_1 \mathbf{U} \varphi_2) \in q \}$ を全て含む

$F = \{\{1, 2, 5, 6, 7, 8\}\}$ となる。

Question

LTL 式 $\varphi = \mathbf{X}\mathbf{X}p$ をオートマトンに変換することを考える。
オートマトンの初期状態、及び各状態からの遷移を答えよ。

Q) 初期状態を答えよ。

Q) 状態 $1$ からの遷移を答えよ。

Q) 状態 $2$ からの遷移を答えよ。

Q) 状態 $3$ からの遷移を答えよ。

Q) 状態 $4$ からの遷移を答えよ。

Q) 状態 $5$ からの遷移を答えよ。

Q) 状態 $6$ からの遷移を答えよ。

Q) 状態 $7$ からの遷移を答えよ。

Q) 状態 $8$ からの遷移を答えよ。

最終的なオートマトンはこのようになる。
7.10 のアルゴリズムを使うとこのオートマトンを簡単にできる。

7.10 Efficient Translation of LTL into Automata #

モチベーション:

  • LTL 式の変換したオートマトンのサイズを小さくしたい
    • 7.9 のアルゴリズムで出力されるオートマトンは、LTL 式の部分式の数に対して指数で増える
      • それぞれの部分式に対して、それ自身とそれの否定を考える必要あり
    • この指数爆発は回避可能
      • 回避できないケースもあるが

直感を養うための具体例:

Example 7.11
  • LTL 式 $\varphi = \mathbf{X}\mathbf{X}p$ を考える
  • $\varphi$ の部分式は $\{ \mathbf{X}\mathbf{X}p, \mathbf{X}p, p \}$
  • 7.9 の粗いアルゴリズムだと $2^3 = 8$ の状態が必要
    • Ref) 1 つ前のクイズ
  • この LTL 式の直感的な解釈は以下
    • 初期状態 : $\varphi = \mathbf{X}\mathbf{X}p$ が成立
    • 次状態 : $\mathbf{X}p$ が成立
    • 次状態 : $p$ が成立
  • これらに加えて “empty” な状態があれば良い
    • “empty” : $p$ に到達したあとの状態 (= 何も条件を課さない状態)

新しいアルゴリズムを理解するための観察 #

7.10 では、LTL 式は negation normal form (NNF) で与えられていると仮定する。

NNF:

  • 否定が atomic proposition にのみ適用されている形
  • ref) MC 本 p42, 4.2.4
  • e.g.)
    $\lnot ((A \mathbf{U}B) \lor \mathbf{F}C) \equiv (\lnot (A \mathbf{U}B) \land \lnot\mathbf{F}C) \equiv (((\lnot A)\mathbf{R}(\lnot B)) \land (\mathbf{G}\lnot C))$

(復習) until ($\mathbf{U}$) や release ($\mathbf{R}$) は不動点の形で書ける

すなわち、以下のように書けるということ:

  • $\mu \mathbf{U} \eta = \eta \lor (\mu \land \mathbf{X}(\mu \mathbf{U}\eta))$
  • $\mu \mathbf{R} \eta \equiv \mu \land (\mu\lor \mathbf{X}(\mu \mathbf{R} \eta)) \equiv (\eta \land \mu) \lor (\mu \land \mathbf{X}(\mu \mathbf{R} \eta))$
    • NNF に落とし込むため、$\mathbf{U}$ と $\mathbf{R}$ の両方が必要。
      • ref) 教科書 p42, 4.2.4

このことから、以下の 2 点を観察できる:

  • 条件を分割できる
    • 式通りの意味
  • 特に、条件を i)現在の状態 ii)次の状態 で分割できる
    • $\mathbf{U}$ での第 2 項に着目
      • 現在の状態で $\mu$ が成立、かつ次の状態で $\mu \mathbf{U} \eta$ が成立

この観察を基に、アルゴリズムで使用するデータ構造を考える。

使用するデータ構造 #

ノードを使ってオートマトンの状態を作り上げる。
(以下では、変換対象の LTL 式を $\varphi$ とし、注目しているノードを $q$ とする。)

フィールド説明
$ID$各ノードで一意な値
$Incoming$$q$ に遷移してくるノードの集合 ($q$ が初期状態の場合は $\{init\}$ )
$New$$\varphi$ の部分式の集合 (未処理); このノード ($q$) から成立する必要あり
$Now$$\varphi$ の部分式の集合 (処理済み);このノード ($q$) から成立する必要あり
$Next$$\varphi$ の部分式の集合 (処理済み); 次のノードから成立する必要あり

さらに、ノードを $Open$ と $Closed$ に分類し、アルゴリズムを適用していく。

Type
$Open$処理中のノードの集合
(処理中はフィールドの値が変化する)
$Closed$処理済み (= $New$ が空) のノードの集合
(構築するオートマトンの状態となる)

オートマトンの構築が完了した段階で、以下の式の成立が保証される (ようにアルゴリズムが作られている):

$$ Prop(q) = \bigwedge q.New \land \bigwedge q.Now \land \mathbf{X}\bigwedge q.Next $$

アルゴリズム (擬似コード) #

Nodeの定義:

1class Node:
2    ID: str  # or int
3    Incoming: set[Node]
4    New: set[LTL]
5    Now: set[LTL]
6    Next: set[LTL]

核となるアルゴリズム:

 1Closed: set[Node]
 2Open: set[Node]
 3
 4def EfficientLTLBuchi(phi: LTL) -> Automata:
 5    """
 6    Efficient translation of LTL to generalized Buchi automaton
 7    """
 8    q: Node
 9    sub_ltl: LTL
10    Closed: set[Node] = set()  # global
11    Open: set[Node] = {Node(n0, {init}, {phi}, {}, {})}  # global
12
13    while len(Open) != 0:
14        q = Open.pop()  # Chose (and delete) q from Open
15        if len(q.New) == 0:
16            Update_Closed(q)
17        else:
18            Open.add(q)
19            sub_ltl = q.New.pop()  # Chose (and delete) sub_ltl from q.New
20            q.Now.add(sub_ltl)
21            Update_Split(q, sub_ltl)
22
23    F: Generalized_Buchi_acceptance_constraints
24    A: Automata = Build_Automaton(Closed, F)
25    return A

Closed を更新するアルゴリズム:

 1def Update_Closed(q: Node):
 2    """
 3    q.New が空であることに注意。
 4    2つの場合がある:
 5    1. あるノード q_ が Closed に存在して、q_.Now == q.Now かつ q_.Next == q.Next な場合
 6       この場合、Prop(q_) == Prop(q) なので、q は Closed に追加しない (状態がダブってしまうため)。
 7       ただし、q.Incoming は q_.Incoming に追加する。
 8    2. その他の場合
 9       q を Closed に追加し、q の後続ノード (q_new) を新規作成、Open に追加する。
10         - q_new.Now = q.Next
11         - q_new.Incoming = {q}
12       ただし、1 の場合同様、状態がダブル場合は追加しない。
13    """
14    if ("q_ s.t. Prop(q) == Prop(q_) exists in Closed"):
15        # When q_ s.t. q.Now == q_.Now and q.Next == q_.Next exists in Closed
16        q_.Incoming = q_.Incoming | q.Incoming  # union
17    else:
18        Closed.add(q)
19        q_new: Node = Node(freshId, {q}, q.Next, {}, {})
20        if ("q_ s.t. Prop(p) == Prop(q_) exists in Open"):
21            # When q_ s.t. q.New == q_.New exists in Open
22            q_.Incoming = q_.Incoming | q.Incoming
23        else:
24            Open.add(q_new)

Open を処理するアルゴリズム:

 1def Update_Split(q: Node, phi: LTL):
 2    """
 3    "X μ" と "μ ∨ η" が本質
 4    "μ U η" や "μ R η" はこれを用いて書ける
 5    """
 6    q_: Node = None
 7    match phi:
 8        case "p or ¬p":  # where p ∈ AP
 9            return
10        case "X μ":
11            q.Next.add(μ)
12        case "μ ∨ η":
13            q_: Node = Split(q)
14            q.New.add(μ)
15            q_.New.add(η)
16        case "μ ∧ η":
17            q.New.add({μ,η})
18        case "μ U η":
19            q_: Node = Split(q)
20            q.New.add(η)
21            q_.New.add({μ, X(μ U η)})
22        case "μ R η":
23            q_: Node = Split(q)
24            q.New.add({μ,η})
25            q_.New.add({η, X(μ R η)})
26    if q_:
27        Open.add(q_)
28
29
30def Split(q: Node) -> Node:
31    """
32    ID 以外が同一な Node を返す
33    """
34    return Node(freshId, q.Incoming, q.New, q.Now, q.Next)

アルゴリズム図解 #

アルゴリズムの動作を図を用いて理解する。

Examples & Questions

LTL 式 $A\mathbf{U}B$ に対してアルゴリズムを適用することを考える。

受理状態集合の構築 #

モチベーション:

  • 状態間の遷移関係は正しい
    • e.g. $\mathbf{X}\mu$ が成り立つなら、次状態では $\mu$ が成り立つような遷移を作っている
  • しかし、パスで見た時、$\mu \mathbf{U} \eta$ の $\eta$ がいつか必ず成り立つ保証はない
  • 受理状態で上記を保証する
    • e.g. $\mu \mathbf{U} \eta$ が成り立つ状態をを通るパスでは、いつか必ず $\eta$ が成立することを保証する

受理状態集合の決め方:

  • 全ての $\mu \mathbf{U} \eta$ の形の LTL 部分式それぞれに対し、
    以下を満たし $Closed$ にあるノードの集合を、受理状態集合の一要素とする(Generalized Buchi Automata):
    1. ($\mu \mathbf{U} \eta$ が $Now$ に入っていて、かつ) $\eta$ が $Now$ にある、or
    2. $\mu \mathbf{U} \eta$ が $Now$ に入っていない

補足:

  • 以上により、$\mu \mathbf{U} \eta$ が途中で成立したら、$\eta$ が成立するまで実行は受理されない
    • $Now$ における $\mu \mathbf{U} \eta$ の形の性質は ($\eta$ が $Now$ に現れるまで) 次状態に引き継がれる

オートマトンの構築 #

流れ:

  1. ノードからクリプキ構造を構築
  2. クリプキ構造を Generalized Buchi オートマトンに変換
    • すでに学習済みのアルゴリズムを使用する
  3. (必要であれば) Non-generalized Buchi オートマトンに変換
    • すでに学習済みのアルゴリズムを使用する

ノードからクリプキ構造 $M = (S, S_0, R, AP, L, F)$ への変換:

  • $S$ : $Closed$ にあるノード集合
  • $S_0$ : $S_0 = \{ q \in S | init \in q.Incoming \}$
  • $R$ : $(q, q’) \in R \iff q \in q’.Incoming$
  • $AP$ : $\varphi$ における atomic proposition の集合。つまり、$AP = \{ p | p \in AP_{\varphi} \}$
    ただし、$\overline{AP} = \{ \lnot p | p \in AP \}$
  • $L$ : $L(q) = q.Now \cap (AP \cup \overline{AP})$
  • $F$ : 全ての $\mu \mathbf{U} \eta$ の形の部分式に対して、$F$ は以下の集合を含む:
    $P_{\mu \mathbf{U}\eta} = \{ q | \eta \in q.Now \; \mathrm{ or } \; (\mu \mathbf{U}\eta) \notin q.Now \}$
Question

以下の処理済みのノードからクリプキ構造を構築する。

以下は構築途中のクリプキ構造である。

遷移を答えよ。

受理状態集合(or公平性制約) $F$ を求めよ。
$F = \{\{q_0, q_2\}\}$
  • $F$ : 全ての $\mu \mathbf{U} \eta$ の形の部分式に対して、$F$ は以下の集合を含む:
    $P_{\mu \mathbf{U}\eta} = \{ q | \eta \in q.Now \; \mathrm{ or } \; (\mu \mathbf{U}\eta) \notin q.Now \}$
  • $A\mathbf{U}B$ は本質的には $(\lnot h) \mathbf{U} c$ と同じ
  • 教科書p74, Figure6.1 の Tableau や 教科書p100, Figure7.10 のオートマトンとの比較
    • 状態数が大幅に削減できている

その他コメント #

7.10 でのアルゴリズムとの重要な差分:

  • ここでのオートマトンは “3-valued automaton” と解釈できる
    • $p \in AP$ は
      1. positive (as $p$)
      2. negative (as $\lnot p$)
      3. not appear (don’t care)
  • この don’t care により、状態数を大幅に減らせる

7.11 On-the-Fly Model Checking #

これまで見てきたモデル検証の方法：

  1. システムのモデルをオートマトン $\mathcal{A} $ に変換する。
  2. 調べたい性質 $\varphi$ の否定をオートマトン $\mathcal{S}$ に変換する。
  3. $\mathcal{A}$ と $\mathcal{S}$ の intersection を取り、それが空かどうかチェックする。
    • 空でなければ、反例が出力される。

On-the-Fly model checking:

  1. 性質の否定を表すオートマトン $\mathcal{S}$ を作る。
  2. オートマトン $\mathcal{A}$ を作る過程で、逐一intersection を計算し、空かどうかチェックすることでガイドする。
    • 空でなかったら(=反例が見つかったら)、オートマトンの作成を中断できる。
    • $\mathcal{A}$ の全ての状態を生成する必要はない
      • $\mathcal{S}$ との intersection で登場しない状態がある

具体的な方法 #

前提(と復習):

  • システムのオートマトンを $\mathcal{A}$ とする
    • 受理状態 : すべての状態
  • 証明したい性質の否定を $\mathcal{S}$ とする
  • $\mathcal{A}$ と $\mathcal{S}$ の intersection の状態が受理状態
    $\iff$ $\mathcal{S}$ 由来の状態が受理状態
  • $\mathcal{S}$ はすでに構築済み

On-the-Fly model checkingでは:

  • intersection の状態の構築は DoubleDFS アルゴリズムと同時に行われる
    • DoubleDFS の遷移先が未計算だったら、intersection を計算

以下は具体的な流れ:

  • $s = (r, q)$ を DoubleDFS の探索途中における状態とする
    • $r$ は $\mathcal{A}$ の状態
    • $q$ は $\mathcal{S}$ の状態
  • $s$ の次状態を 1 つずつ計算する
    • $\mathcal{S}$ における $q$ の次状態 $q_1, q_2, \dots, q_n$ は計算済み
    • $r$ の次状態 : $r'$
  • $s$ の次状態は $s_i = (r', q_i)$ (ただし $1 \leq i \leq n$ ) は、$r$ から $r'$ への遷移と $q$ から $q_i$ への遷移が同じラベルな時にのみ存在する

DoubleDFS アルゴリズムの探索空間の削減は以下の 2 パターン:

  1. $r'$ のラベルがどの $q_i$ とも合致しない。
    この場合、$r'$ 以降の状態の探索を行わない。
  2. サイクルが見つかった場合。
    反例が見つかったので、$\mathcal{A}$ の構築は中断できる。

以上のようにして、性質を表すオートマトン $\mathcal{S}$ を用いて $\mathcal{A}$ の構築を省力化できる。

その他コメント #

  • 明示的に状態を扱うモデル検証(explicit-state model checking)では非常に効率的
  • 記号モデル検証(symbolic model checking, BDD や SAT ベースの方法)では役に立たない
Calendar May 24, 2023