| 研究概要 |
本研究の目標であるcardinality analysisを一般化し、様相論理式をmin-plus代数N∞を用いて解釈する意味論について研究を行った。N∞は、自然数の全体に要素∞を追加して得られるmin-plus代数である。この意味論のもとでは、∧はmin-plus代数のplus演算、∨はmin演算によて解釈され、様相論理式[f]φのノードsにおける解釈が、sから様相fによって到達可能なノードにおけるφの解釈を足し合わせたものになる。すると、φを満たすノードの数は、大域的様相oを用いて、[o](〓φ∨1)という様相論理式の解釈として表すことができる。この意味論を用いると、様相論理式を満たすノードの数だけでなく、たとえばノードからノードへの最短経路の長さなども様相論理式によって表現できる。本年度は特にmin-plus代数上の様相μ計算のモデル検査アルゴリズムを考案し実装した。min-plus代数N∞は上には整礎ではないので、モデル検査で通常用いられる単純な反復アルゴリズムは停止しないため、抽象解釈と組み合わせたモデル検査アルゴリズムを考案した。モデル検査アルゴリズムに関しては、コンパイラにおけるフロー解析への応用について検討した。さらに、論理式φとプログラムσに対して、その最弱事前条件wp(σ,φ)を、σを実行する前のwp(σ,φ)の解釈と実行後のφの解釈がmin-plus代数上で等しくなるように定義した。そして、 wp(σ,φ)の解釈がφの解釈より小さくなるための十分条件を定式化した。N∞は下には整礎であるので、この方法を用いて、cardinalityだけでなく、さまざまな尺度による停止性解析および活性解析が可能となった。
|
