by Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv and Sharon Shoham
Propositional classical logic で記述された LTS の invariant 発見問題についての計算量や情報理論による解析。遷移関係 については black-box として扱い、Hoare triple
が成立するかどうか（成立しない場合は反例も返す）を使って invariant を探すという設定。
概要
上記の設定において「多項式長の invariant を探す問題」について考察している。主結果は次の通り。
- こうした推論問題においては invariant 候補をいかに上手く一般化するかが（実用上の）鍵になるが、上記の設定において性能の改善できるような一般化方法はない。問題を解くには指数回の Hoare クエリを必要とする。
- PDR と ICE の推論方法を比較すると、PDR の方が指数的に優れている例が存在する。
後者において PDR と ICE の違いをどこに求めるかが一つの焦点であるが、本論文では Hoare クエリの種類の違いが本質的であるという観察をしている。つまり、PDR では で
の場合も用いるが、ICE では
（つまり
が invariant であるか）しか用いない。この差が本質的な違いとなって、先述の指数的な差を生む。
（設定さえ上手くできれば）前者についてはそんなものだろうという気がする*1ので、後者について解説する。
差がつく例として利用されるのは、本論文で maximal systems for monotone invariant と呼ばれる種類の遷移系である。monotone invariant というのは、二値ブール代数 を
という順序集合として理解したときに、invariant が
という関数として anti-monotone であることを指す。遷移系が invariant
に対して maximal であるとは、
であること、つまり任意の
を満足する２状態は直接遷移可能で、さらに任意の
を満足しない２状態も直接遷移可能である場合である。こうしたシステムの invariant 発見は非常に簡単で、初期状態の１ステップ forward image を計算すれば、それが invariant である。
forward image の計算は Hoare クエリそのものではないが、実は上手く Hoare クエリを繰り返すことで forward image が計算できる。PDR のように事前条件と事後条件に別のものを指定するクエリを利用すれば、（事前条件は初期状態に固定して） というクエリによって
が invariant の過大近似であるかどうかを判定することができる。実際に invariant に入っている点
（だけからなる singleton を表す性質）から初めて、変数の個数回ほど上記クエリを発行して２分探索を行うことにより、
を conjunctive normal form で書いたときの節を１つ見つけることができる*2。これを
の節の個数回だけ繰り返せば
が得られる。
一方で ICE 型のクエリではこのようにして forward image を計算することはできず、一般の場合と同様の理由で指数回のクエリが必要となってしまう。
なお論文では Hoare クエリよりも少し強力な interpolation クエリについても議論されており、こちらでもやはり指数回のクエリ呼び出しを必要とするケースがあることが示されている。
感想
文句ない POPL paper だなあという内容であった。分析手法は新しく面白いし、概要は Sections 1, 2 を読めば概ね分かるので、興味のある人は読むのを勧める。PDR と ICE の効率の差を理論的に示せると考えたことはなかったので、結果は非常に印象的であった。一方で、証明手法を読んでいると、妥当そうな仮定を積み重ねて現実から離れたところに行ってしまったという印象を受けた。仮定のうち現実にそぐわないものとしては、例えば遷移関係 が見えないという仮定*3やその複雑さが無制限であるという仮定*4が挙げられるだろう。また本論文の解析手法を整数等の無限データがある場合にどのように拡張することができるかも、興味深い非自明な問であろう。
余談だが、てっきり distinguished paper かと思っていたら、そうではなかったらしい。個人的には distinguished paper の水準にあると思う。
