| 研究概要 |
今年度の研究成果は下記の通り.
1.確率システムのモデルの一般化である確率的多重関係と通常の二項多重関係との間のガロア接続が3つ得られた.確率システムの検証手法の実用化には,モデルの大胆な抽象化が不可欠である.ガロア接続は抽象化の健全さを保証する抽象解釈のベースとなる相互関係であり,具体集合,抽象集合と呼ばれる2つの半順序集合と,抽象化,詳細化に相当する2つの単調写像によって定義される.抽象化写像が具体集合の任意の上限を保つとき,詳細化写像は一意に定まる.本研究では具体集合を確率的多重関係として,抽象集合を「全域的な上向きに閉じた有限二項多重関係」としたガロア接続を2つ((1)及び(2)とする),抽象集合を「底を含む和と下向きに閉じた有限な底付き二項多重関係」としたガロア接続を1つ((3)とする)発見した.
2.完備べき等左半環の演算はプログラムにおける基本的な演算に対応している.上記のガロア接続に現れる3つのモデルがいずれも完備べき等左半環をなすことから,抽象化・詳細化によって保たれる演算や性質について調べた.その結果,3つのガロア接続のうち(3)を用いた抽象化が最も有用であることが分かった.その理由は次の(ア)～(ウ)による.
(ア)(1)～(3)における抽象化写像は全て完備べき等左半環準同型.(イ)(1)の場合,抽象化前には一般に成り立たない性質(右分配則)が,抽象化後には常に成り立つ一方,(2),(3)ではこのような現象が起きない.(ウ)(1),(3)の場合,詳細化写像が完備べき等左半環の演算の1つである"1"を保つ.1はプログラムにおいてはSkip(何もしないプログラム)に相当する.
(1)～(3),いずれの場合も詳細化写像が他の演算を保つかは分かっていない.今後は,この点を調査するとともに,より適切な抽象領域とガロア接続について検討する.また,得られたガロア接続を実際の検証に適用した上でその検証能力を調べる.
|
