|
本研究では，1. 並行システムの多重関係モデルに基づくテストの概念の準等式系による特徴づけ，2. 様相論理の近傍意味論の知見を用いた様相演算子の準等式系による特徴づけ，3. 並行クリーニ代数(CKA)の並行合成を見直すことによる模倣等価性への対応付け，4. 項目3までに導入した演算子の相互作用の洗い出しおよび準等式系としての表現，5. 項目4までで得られた代数構造の自由生成の具体的な構成の5項目について4年間かけて取り組むことにしている．今年度は2，3，4を実施した．
動的論理はプログラムを検証するための論理体系として提案された．動的論理の肝要な要素のみを1階の準等式公理系として抽出したのがテスト付クリーニ代数（KAT）であり，動的論理を並行計算に適用できるように拡張したのが並行動的論理である．並列合成を持つ点と，その意味論が二項多重関係の上で展開される点の2点が動的論理と大きく異なる．動的論理の骨格を抜き出して得られるのがKATであるのに対して，並行動的論理の骨格を抜き出して得られる構造は明らかになっていない．
Peleg らが用いたモデルは逐次合成の結合律が成り立たないなど多少不自然な点がある．このうち結合律が成り立つための十分条件を明らかにした．また，Goldblatt の論文を参考に並行動的論理の2種類の様相演算子の間の双対性を仮定しない場合について検討し，Goldblatt の論文に誤りがあることを具体例を与えることにより明らかにした．
|
