|
本研究では4年間で，1. 並行システムの多重関係モデルに基づくテストの概念の準等式系による特徴付け，2. 様相論理の近傍意味論の知見を用いた様相演算子の準等式系による特徴付け，3. 並行クリーニ代数（CKA）の並行合成を見直すことによる模倣等価性への対応付け，4. 項目3までに導入した演算子の相互作用の洗い出しおよび準等式系としての表現，5. 項目4までで得られた代数構造の自由生成の具体的な構成，の5項目について順次取り組むことにしている．このうち，今年度は1と2を実施した．
動的論理はプログラムを検証するための論理体系として提案された．動的論理の肝要な要素のみを１階の準等式公理系として抽出したのがテスト付きクリーニ代数（KAT）であり，動的論理を並行計算に適用できるように拡張したのが並行動的論理である．並行合成を持つ点と，その意味論が二項多重関係の上で展開される点の2点が動的論理と大きく異なる．動的論理の骨格を抜き出して得られるのがKATであるのに対して，並行動的論理の骨格を抜き出して得られる構造は明らかになっていない．今年度はPelegやGoldblattによる論文を参考に，並行動的論理の骨格を抜き出すことを試みた．彼らが採用した二項多重関係の逐次合成が大変煩雑であったため，研究協力者の助言により定理証明系Isabelleを用いて証明の各ステップを形式化しながらの作業となった．このことにより，並行動的論理の骨格を抜き出すことに成功しただけでなく，Goldblattの論文にある誤りを発見することもできた．この論文の誤りを修正できるかどうかも，興味深い問題である．
現在，ここまでで得られた成果をまとめた論文の執筆作業中である．
|
