研究課題
本研究では，1. 並行システムの多重関係モデルに基づくテストの概念の準等式系による特徴づけ，2. 様相論理の近傍意味論の知見を用いた様相演算子の準等式系による特徴づけ，3. 並行クリーニ代数(CKA)の並行合成を見直すことによる模倣等価性への対応付け，4. 項目3までに導入した演算子の相互作用の洗い出しおよび準等式系としての表現，5. 項目4までで得られた代数構造の自由生成の具体的な構成，の5項目について4年間かけて取り組むことにしている．今年度は昨年度に引き続き1と2を実施し，新たに3も実施した．動的論理はプログラムを検証するための論理体系として提案された．動的論理の肝要な要素のみを1階の準等式公理系として抽出したのがテスト付クリーニ代数（KAT）であり，動的論理を並行計算に適用できるように拡張したのが並行動的論理である．並列合成を持つ点と，その意味論が二項多重関係の上で展開される点の2点が動的論理と大きく異なる．動的論理の呼格を抜き出して得られるのがKATであるのに対して，並行動的論理の骨格を抜き出して得られる構造は明らかになっていない．昨年度の作業で並行動的論理の骨格を必要最低限抜き出すことに成功していたので，これを論文にまとめて投稿した．さらに，並行合成と領域演算子や様相演算子の関連性をあきらかにした．
2: おおむね順調に進展している
定理証明系を効果的に利用することにより，おおむね予定していたペースで研究を実施できている．
Peleg らが用いたモデルは逐次合成の結合律が成り立たないなど多少不自然な点があるので，より自然なモデルを探す必要がある．並行動的論理の2種類の様相演算子の間の双対性を仮定しない場合についても検討する．
すべて 2015 2014 その他
すべて 雑誌論文 (5件) (うち査読あり 3件、 謝辞記載あり 5件、 オープンアクセス 2件) 備考 (1件)
Journal of Logical and Algebraic Methods in Programming
巻: 84 ページ: 426-439
doi:10.1016/j.jlamp.2014.08.008
巻: 84 ページ: 359-376
doi:10.1016/j.jlamp.2014.12.003
Computing Research Repository (CoRR), arXiv.org
巻: 1501. 05147 ページ: 1-34
Lecture Notes in Computer Science, Springer
巻: 8428 ページ: 261-273
10.1007/978-3-319-06251-8_16
巻: 1407. 5819 ページ: 1-44
http://www.sci.kagoshima-u.ac.jp/~furusawa/person/research.html
