ωオートマトン

オートマトンは入力を受け付けるかどうかを問題にするので計算は有限時間に終わる。

しかし、サーバなどの計算は終了することは想定されてない。入力が無限にある場合を考えたい。

例えば、信号機は停まらずにずーっと動くことが期待されていて、正しい信号機の動作とそうでない動作がある。そして信号機はオートマトン的に動作している。

ωオートマトンと様相論理

これらは時間の様相を表す論理に関係している。

　　　　[] p ずーっとpが成立する　　　　<> p いつかpが成立する

これを組み合わせると

　　　　<> [] p いつからか、ずーっとpが成立するようになる　　　　[] <> p ずーっと、いつかpが起きる

[] はbox、<>はdiamonと呼ばれたりする。

        [] p = ¬ ( <> ¬ p )
        <> p = ¬ ( [] ¬ p )

である。[] <> p をωオートマトンとして考えることができる。

                       ¬ p
                   ------------>
        [] <> p *                 [] <> p 
                   <-----------
                       p

p と ¬ p で二つの状態 ( [] <> p * と [] <> p)を行き来する。

    data  States3   : Set  where
       ts* : States3
       ts  : States3
    transition3 : States3  → Bool  → States3
    transition3 ts* true  = ts*
    transition3 ts* false  = ts
    transition3 ts true  = ts*
    transition3 ts false  = ts
    mark1 :  States3  → Bool
    mark1 ts* = true
    mark1 ts = false
    ωa1 : Automaton States3 Bool
    ωa1 = record {
            δ = transition3
         ;  astart = ts*
         ;  aend = mark1
      }

ここで、[] <> p * ( 上では ts* ) を無限回通れば、 [] <> p が成立していることになる。(Buchi automaton )

これの否定は、<> [] ( ¬ p ) ということになる。これは、ある時点からずーっと ¬ p が続く。(Muller automaton )

ωオートマトンの定義

オートマトンの定義は同じものを用いる。ただし、入力は無限にある。

    record Automaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
            δ : Q → Σ → Q
            astart : Q
            aend : Q → Bool

automaton の定義にはもともと入力の実装が何かは記述されていない。

Agda では無限の長さのリストを扱うことはできない。その代わり、自然数 n から入力Σを生成する関数( ℕ → Σ )を用いる。これを用いて、

    ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
    ω-run Ω zero s = astart Ω
    ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )

と言う形でオートマトンが無限に実行される。

この無限長の入力をどう受け付けるかを定義する必要がある。これには二通りの方法がある。

    record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
        field
            from : ℕ
            stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x S n ) ≡ true
    record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
        field
            next     : (n : ℕ ) → ℕ
            infinite : (x : Q) → (n : ℕ ) →  aend Ω ( ω-run Ω x  S (n + (suc (next n)))) ≡ true

Muller ではある時刻から先では、aend で定義される状態の集合にずーっと留まる。Buchi ではaendで定義されるある状態の集合を無限回通る。

Muller automaton と Buchi automaton の関係

    B→M : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q 
        → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )
    M→B : { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q 
        → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S )

これが証明できる