たまにゃんのメモ帳

情報系関連のメモ書きを主に載せていきます。あわよくば他の人の参考になれば...

The ComBack Method – Extending Hash Compaction with Backtracking (2007)

URL : http://link.springer.com/content/pdf/10.1007%2F978-3-540-73094-1_26.pdf

大雑把にいえば状態を持たずにハッシュ値と状態の一意のID(整数)と状態へのバックエッジ(遷移関数、前の状態の一意のID)を持ち、ハッシュ値がぶつかった場合バックエッジで最初の状態root(かもしくはキャッシュされた状態)へたどり再度状態を復元する手法。
状態遷移が軽く、状態のメモリ消費量が多いモデル検査においては非常に効果を発揮しそう。

  1. Abstract
    • ComBack Method は Hash Compaction を拡張し、状態空間のすべてのカバレッジが保証するような手法。
    • それぞれの状態を一意で表現する整数と展開前の状態へのバックエッジを保持する。
    • これで、バックトラックを使うことですべての状態識別子を構築しなおし、Hash Compaction のハッシュ衝突の問題を on-the-fly に解決する
  2. Background
    • Hash Compaction Method
      • Hash Compaction の基本的なアイデアは状態Sから固定サイズのbit-stringの集合にマップする関数Hを使うこと
      • それぞれ訪問した状態sに対して、状態管理表にを完全な状態識別子を登録するのではなく、ハッシュ値のみを保存する
  3. The ComBack Method
    • 完全な状態識別子を持つことなく、オンデマンドにバックトラックキングを使うことで状態管理表に完全な状態識別子を再構築し、ハッシュの衝突を解決する。
    • 完全な状態識別子を再構築するには以下のやり方を用いる
      1. すべての訪問した状態にstate number N(s)を割り当てる
      2. state tableはそれぞれの圧縮状態識別子のcollision listを保存する。collision listとはこの圧縮状態識別子へマップされた訪問先の状態へのstate numberのリストである。
      3. backedge table は訪問された状態へのバックエッジを保存する。状態 s への backedge は transition t と state number nで構成されている。前の状態を s' とすると s' (t)→ s
  4. The ComBack Algorithm
m ← 1
StateTable.Init() StateTable.Insert(H(sI),1)) 
WaitingSet.Init() WaitingSet.Insert(sI,1) 
BackEdgeTable.Init() BackEdgeTable.Insert(1, ⊥)
while ¬ WaitingSet.Empty() do
    (s, n′ ) ← WaitingSet.Select()
    for all t,s′ such that (s,t,s′) ∈ ⊿ do
        if ¬ Contains(s′) then
            m←m+1 StateTable.Insert(H(s′), m) 
            WaitingSet.Insert(s′, m) 
            BackEdgeTable.Insert(m, (n′ , t))

proc Contains(s′) is
    for all n ∈ StateTable.Lookup(H(s′)) do
        if Matches(n, s′) then 
            return tt
        return ff

proc Matches(n, s′) is
    return s′ = Reconstruct(n)
                    
proc Reconstruct(n) is 
    if n = 1 then
        return sI 
    else
        (n′ , t) ← BackEdgeTable.Lookup(n) 
        s ← Reconstruct(n′)
        return Execute(s,t)