|
動的論理はプログラムを検証するための論理体系としてFischerとLadnerによって提案された．動的論理の肝要な要素のみを１階の準等式公理系として抽出したのがKozenのテスト付きクリーニ代数（KAT）である．KATは，命題ホーア論理を包含するためホーア論理の推論の大部分を等式変形により行うことが可能であり，プログラムの部分正当性検証やコンパイラの正当性検証などに用いられる．
動的論理を並行計算に適用できるように拡張したのが並行動的論理であり，Pelegによって提案された．並行合成を持つ点と，その意味論が二項多重関係の上で展開される点の2点が動的論理と大きく異なる．動的論理の骨格を抜き出して得られるのがKATであるのに対して，並行動的論理の骨格を抜き出して得られる構造は明らかになっていない．
Pelegらが用いたモデルは逐次合成の結合律が成り立たないなど多少不自然なところがある．昨年度に引き続き，今年度も不自然さの解消に取り組んだ．その結果，昨年度中に明らかにしていた結合律成立の十分条件を，クライスリ・トリプルの観点から寓圏の枠組みの中できれいに整理することに成功した．また，逐次合成と並行合成の間の相互作用を新たに発見したので，これを利用して以前与えた準等式公理系を拡張し，領域演算子の明示的な定義を与えることに成功した．これにより，逐次合成に関する部分単位のクラス，並行合成に関する部分単位のクラス，停止元のクラス，非停止元のクラスの関連性を明らかにすることができた．昨年度明らかにしたGoldblattの論文の誤りの修正も試みたが成功には至らなかった．
|
