|
127
|
1 -title: ωオートマトン
|
|
|
2
|
|
|
3 オートマトンは入力を受け付けるかどうかを問題にするので計算は有限時間に終わる。
|
|
|
4
|
|
|
5 しかし、サーバなどの計算は終了することは想定されてない。入力が無限にある場合を考えたい。
|
|
|
6
|
|
|
7 例えば、信号機は停まらずにずーっと動くことが期待されていて、正しい信号機の動作とそうでない動作がある。そして信号機はオートマトン的に動作している。
|
|
|
8
|
|
|
9 --ωオートマトンと様相論理
|
|
|
10
|
|
|
11 これらは時間の様相を表す論理に関係している。
|
|
|
12
|
|
|
13 [] p ずーっとpが成立する
|
|
|
14 <> p いつかpが成立する
|
|
|
15
|
|
|
16 これを組み合わせると
|
|
|
17
|
|
|
18 <> [] p いつからか、ずーっとpが成立するようになる
|
|
|
19 [] <> p ずーっと、いつかpが起きる
|
|
|
20
|
|
|
21 [] はbox、<>はdiamonと呼ばれたりする。
|
|
|
22
|
|
|
23 [] p = ¬ ( <> ¬ p )
|
|
|
24 <> p = ¬ ( [] ¬ p )
|
|
|
25
|
|
|
26 である。[] <> p をωオートマトンとして考えることができる。
|
|
|
27
|
|
|
28 ¬ p
|
|
|
29 ------------>
|
|
|
30 [] <> p * [] <> p
|
|
|
31 <-----------
|
|
|
32 p
|
|
|
33
|
|
|
34 p と ¬ p で二つの状態 ( [] <> p * と [] <> p)を行き来する。
|
|
|
35
|
|
|
36
|
|
|
37 data States3 : Set where
|
|
|
38 ts* : States3
|
|
|
39 ts : States3
|
|
|
40
|
|
|
41 transition3 : States3 → Bool → States3
|
|
|
42 transition3 ts* true = ts*
|
|
|
43 transition3 ts* false = ts
|
|
|
44 transition3 ts true = ts*
|
|
|
45 transition3 ts false = ts
|
|
|
46
|
|
|
47 mark1 : States3 → Bool
|
|
|
48 mark1 ts* = true
|
|
|
49 mark1 ts = false
|
|
|
50
|
|
|
51 ωa1 : Automaton States3 Bool
|
|
|
52 ωa1 = record {
|
|
|
53 δ = transition3
|
|
|
54 ; astart = ts*
|
|
|
55 ; aend = mark1
|
|
|
56 }
|
|
|
57
|
|
412
|
58 ここで、[] <> p * ( 上では ts* ) を無限回通れば、 [] <> p が成立していることになる。(Buchi automaton )
|
|
|
59
|
|
|
60 これの否定は、<> [] ( ¬ p ) ということになる。これは、ある時点からずーっと ¬ p が続く。(Muller automaton )
|
|
|
61
|
|
|
62 --ωオートマトンの定義
|
|
|
63
|
|
|
64 オートマトンの定義は同じものを用いる。ただし、入力は無限にある。
|
|
127
|
65
|
|
412
|
66 record Automaton ( Q : Set ) ( Σ : Set )
|
|
|
67 : Set where
|
|
|
68 field
|
|
|
69 δ : Q → Σ → Q
|
|
|
70 astart : Q
|
|
|
71 aend : Q → Bool
|
|
|
72
|
|
|
73 automaton の定義にはもともと入力の実装が何かは記述されていない。
|
|
|
74
|
|
|
75 Agda では無限の長さのリストを扱うことはできない。その代わり、自然数 n から入力Σを生成する関数( ℕ → Σ )を用いる。
|
|
|
76 これを用いて、
|
|
127
|
77
|
|
|
78
|
|
412
|
79 ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → ℕ → ( ℕ → Σ ) → Q
|
|
|
80 ω-run Ω zero s = astart Ω
|
|
|
81 ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )
|
|
|
82
|
|
|
83 と言う形でオートマトンが無限に実行される。
|
|
|
84
|
|
|
85 この無限長の入力をどう受け付けるかを定義する必要がある。これには二通りの方法がある。
|
|
|
86
|
|
|
87 record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
|
|
|
88 field
|
|
|
89 from : ℕ
|
|
|
90 stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x S n ) ≡ true
|
|
|
91
|
|
|
92 record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
|
|
|
93 field
|
|
|
94 next : (n : ℕ ) → ℕ
|
|
|
95 infinite : (x : Q) → (n : ℕ ) → aend Ω ( ω-run Ω x S (n + (suc (next n)))) ≡ true
|
|
127
|
96
|
|
|
97
|
|
412
|
98 Muller ではある時刻から先では、aend で定義される状態の集合にずーっと留まる。Buchi ではaendで定義されるある状態の集合を無限回通る。
|
|
127
|
99
|
|
412
|
100 --Muller automaton と Buchi automaton の関係
|
|
127
|
101
|
|
412
|
102 B→M : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q
|
|
|
103 → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
|
|
|
104
|
|
|
105 M→B : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q
|
|
|
106 → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
|
|
|
107
|
|
|
108 これが証明できる
|
|
|
109
|
