by Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken
与えられた状態遷移系から、状態上の述語を頂点に持つ遷移系を構成する手法の提案。ならびに、状態上の遷移系の分析と述語上の遷移系の分析を、情報を交換しながら並行して行う手法の提案。
概要
整数変数を持つプログラムのような無限状態遷移系の安全性の自動検証において、パフォーマンスの鍵となるのが適切な述語を見つける問題である。本論文は、双対的な視点からこの問題にアプローチするものである。
ということで、視点を変えて、重要そうな述語の代わりに重要そうな状態を見つける問題を考えてみよう。なにがしかの述語 が与えられている状況を仮定すると、注目すべき状態とは「
が安全性の証拠になっていない」ことを表す状態、例えば
であって
を満たす状態
などが考えられるだろう。状態と述語の役割を逆にすると、この論文が提案する述語発見方法（DualHoudini）になる。この述語発見手法（＝DualHoudini）と、述語候補の集合を入力に取る通常の安全性判定手法（＝PrimalHoudini、つまり普通の Houdini）を交互に実行するのが、本論文による Primal-Dual 版の Houdini である。
状態と述語の役割を逆にするということは、述語を頂点にもつ遷移系を考える必要がある。本論文のポイントは、その定義にある。状態遷移系 と述語遷移系
が与えられたとする*1。ここで
は
上の述語の集合の適当な部分集合である。ただし各
は
上で真であることを仮定する。これらが双対であるとは、
が成り立つことと定義される*2。面白いのは次の性質である：
かつ
ならば
。つまり、述語の方の遷移系で到達可能な述語たちは、すべての到達可能集合を含んでいる*3。
こうして状態と述語が対称な概念となったので、「安全性に違反する状態に至る状態遷移列を探す技術」を「安全性を証明する述語に至る述語遷移列を探す技術」だとみなすことができるようになるわけである。この基盤技術として Houdini アルゴリズムを使ったのが本論文である。
ひとつ注意しておくこととしては、述語上の遷移関係 *4 は計算が容易ではことが挙げられる。論文ではページを割いて、この遷移系の取り扱いを議論している。
感想
述語の上の遷移系の定義は新しいし面白い。特に「状態遷移系の安全性証明」が「述語遷移系の到達可能性」に帰着することで、「安全性証明に便利な命題探し」を「述語遷移系における初期状態からのパス探し」だとみなす視点の切り替えはすばらしい。
ただ、読み終わってから振り返るに、論文の議論の中には本質からズレたものも多かったのではないだろうかという気がする。例えば論文では、状態遷移系を種として３つの遷移系（述語上の遷移系２つと、状態上の遷移系１つ）を定義して、元の状態遷移系と合わせた４つ組を主に取り扱っているが、私としては導入された３つのうち１つ以外は不要だったように思う。こうした理論展開になっている理由は、たぶん、論文中で「k-indutively provable」と呼ばれている概念に基づく述語遷移系が、状態遷移系の双対として（唯一？ カノニカルな？）述語上の遷移系であるといった主張を展開するためだと思われる。私はこれは違うのではないかと思う。述語遷移系の選択は（双対である限りにおいて）理論的にはなんでも良いとした方がクリアだっただろう（ただし、述語遷移系の選択は計算効率と証明能力に影響するから慎重に行う必要はある）。ということなので、述語遷移系の遷移が何を意味するかとかの議論は軽く流しつつ読むのがオススメである。
*1:記号は論文のものとは異なる
*2:これを双対と呼ぶのは良くないと思う。双対なシステムはひとつではなく、遷移を減らす操作で閉じている。特に、どのような遷移系も遷移が一切ない遷移系と双対である。個人的には、論文の意味で「双対」な中でも最も遷移が多いシステムだけが双対の名にふさわしいと思う。なお、双対の意味を「双対」な中で最も遷移が多いものとしたとしても、双対の双対は元の遷移系とは限らず、一般には元よりも多くの遷移を含む。
*3:実はより強く、到達可能集合を含み、状態遷移で閉じた述語であることまで言える
*4:論文が採用しているもの、あるいは、その他の使えそうなもの。もちろん述語上の遷移関係が空集合でも双対性は満足し、この遷移関係の計算は自明に行えるが、それが誘導する自動検証器の証明能力は０である。
