A linear translation from CTL* to the first-order modal μ-calculus
概要
- mCRL2 http://www.mcrl2.org/ というシステムの研究グループによる論文。
- LTL や CTL* という論理体系の論理式を μ-calculus というのの論理式に変換するとサイズが指数爆発するんだけど
- first-order modal μ-calculus というのを使うと線形サイズで済むよ
- なので世界中の人民は first-order modal μ-calculus の解析器さえ一つ作ればいちいちLTLとかCTL*とか個別に作らなくてもよいので幸せなのであるフハハハハ（誇張）
- 「『μ-calculus もLTLやCTL*を表現できるのでこれ一個あれば…』と言われていたけれど、でも、サイズが指数オーダで大きくなって大変なんでしょう？」みたいな背景がある
時相論理（LTL, CTL, CTL* など）
- ふつうの論理式に加えて、時間に関する言及がある
- X p (次の瞬間には p が成りたつ。neXt)
- p U q (q が成り立つようになるまでは p が成り立ち続ける, Until)
- A p この先世界がどう進もうとも p が成り立つ
- 全部自由にこの時間オペレータをつかっていいのが CTL*
- 最初に必ずA、他の場所ではAを絶対使わない、のがLTL
- CTLはなんだっけ
- プログラムの時間的な仕様を「何かを受信するまでは必ずこの作業をしている」とか、そういう感じで記述するのに使う
- 「これで書いた仕様」と「プログラム」を与えて、ちゃんと仕様を満たすかチェックしてくれる的システムが例えば mCRL2
μ計算
- U とか A とかいちいち個別に考えるの面倒くさいので不動点演算子いれればいいだろオラーという論理
- ◇p (次の瞬間にはpが成り立っているような未来がありうる)
- □p (次の瞬間には必ずpが成り立つ。運命は定まっている)
- μY. ...Y... (その論理式の最小不動点)
- 例: μY.(お腹が減る ∨ □Y)
- お腹が減る ∨ □(お腹が減る ∨ □(お腹が減る ∨ □(...))
- なので、要するに「いつかはお腹が減る」
本題
- 書けるんだけど真面目にエンコードすると論理式の長さが指数サイズになります
- first-order μ計算というものがあれば解決！
μX. ◇X ∨ (p(0) ∧ μY ∨ ◇Y ∨ (p(1) ∧ μZ . ◇Z ∨ p(2)))
- こんな風に、「p が成りたつ」のところを「p(0) が成り立つ」「p(1) が成り立つ」「p(2)が成り立つ」みたいな、データでparameterizeできる
μX(i:0). ◇X(i) ∨ (p(i) ∧ ◇X(i+1)) ∨ i=3
という論理を使うと、
- LTL や CTL* の式を受け取る
- オートマトンに変換する
- オートマトンの状態でparameterizeした変数を使うと線形サイズでオートマトンをμ計算で表現できる
という3ステップで小さく変換できる。オートマトン経由するとめんどいので直接変換のやりかたも論文に書いてあった。
感想
そりゃ表現できるというのはそうだなーという感じなので、むしろ驚くべきなのはfirst-order μ計算がμ計算と同じオーダの効率で検査できるという方かなーと思います。
たぶんその部分の該当論文は：
12. J.F. Groote and R. Mateescu. Verification of temporal properties of processes in a setting with data. In Algebraic Methodology and Software Technology, volume 1548 of LNCS, pages 74–90. Springer, 1998.
15. J.F. Groote and T.A.C. Willemse. Parameterised boolean equation systems. Theoretical Computer Science, 343(3):332–369, 2005.
最終更新：2011年03月06日 11:51
