2014 Fiscal Year Research-status Report
| Project/Area Number |
25330016
|
|---|
| Research Institution | Kagoshima University |
|---|
Principal Investigator |
古澤 仁 鹿児島大学, 理工学研究科, 准教授 (00357930)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 並行計算 / 準等式系 / 動的論理 |
|---|
| Outline of Annual Research Achievements |
本研究では，1. 並行システムの多重関係モデルに基づくテストの概念の準等式系による特徴づけ，2. 様相論理の近傍意味論の知見を用いた様相演算子の準等式系による特徴づけ，3. 並行クリーニ代数(CKA)の並行合成を見直すことによる模倣等価性への対応付け，4. 項目3までに導入した演算子の相互作用の洗い出しおよび準等式系としての表現，5. 項目4までで得られた代数構造の自由生成の具体的な構成，の5項目について4年間かけて取り組むことにしている．今年度は昨年度に引き続き1と2を実施し，新たに3も実施した．
動的論理はプログラムを検証するための論理体系として提案された．動的論理の肝要な要素のみを1階の準等式公理系として抽出したのがテスト付クリーニ代数（KAT）であり，動的論理を並行計算に適用できるように拡張したのが並行動的論理である．並列合成を持つ点と，その意味論が二項多重関係の上で展開される点の2点が動的論理と大きく異なる．動的論理の呼格を抜き出して得られるのがKATであるのに対して，並行動的論理の骨格を抜き出して得られる構造は明らかになっていない．
昨年度の作業で並行動的論理の骨格を必要最低限抜き出すことに成功していたので，これを論文にまとめて投稿した．さらに，並行合成と領域演算子や様相演算子の関連性をあきらかにした．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
定理証明系を効果的に利用することにより，おおむね予定していたペースで研究を実施できている．
|
| Strategy for Future Research Activity |
Peleg らが用いたモデルは逐次合成の結合律が成り立たないなど多少不自然な点があるので，より自然なモデルを探す必要がある．並行動的論理の2種類の様相演算子の間の双対性を仮定しない場合についても検討する．
|
Research Products
(6 results)
