Integrating hybrid logics into concurrent program logic

2023 Fiscal Year Research-status Report

• Project/Area Number: 23K11051
• Research Institution: Chiba Institute of Technology
• Principal Investigator: 安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
• Project Period (FY): 2023-04-01 – 2026-03-31
• Keywords: 並行プログラム論理 / 動的論理

Outline of Annual Research Achievements

本年度は既存研究のサーベイと、既存研究の結果を利用して本研究課題において対象とする並行プログラム論理に対して可能であること不可能であることの切り分け作業に終わってしまい、外部発表をおこなえるだけの十分な研究成果を得ることはできなかった。具体的には、まず逐次プログラム論理を動的論理と見なすよく知られた結果からの類推で並行プログラム論理を動的論理と見なし、その際に並行プログラム論理について非干渉性を保証する Owicki--Gries 条件や rely/gurantee 条件の現れを動的論理の意味論である Kripke 構造で表現することまでは比較的容易にできた。ここで、本年度前半は研究計画に記載したノミナルによる拡張を試してみたところ、表現力自体は変更されないものの表現の簡潔さには寄与しそうであるという感触は得た（証明は未完）。既存研究のサーベイをおこなう作業に関連して、8月に4日間にわたる合宿形式の研究集会を主催し、その筋の専門家から直接レクチャをしてもらう機会をみづからつくった。これらのサーベイと既存研究のアプローチの適用という試行を通して、対象とする並行プログラム論理について特にインストラクションのread-write リオーダリングに関する操作的意味論に対して既存の知識様相論理・動的論理の手法が適用できそうというところまでは至ったので、本年度後半はこれを詰める作業をおこなってきた。

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

ハイブリッド論理のノミナルの利用が並行プログラム論理の拡張にあまり寄与しないという感触を得てしまい、そもそも対象としていた並行プログラム論理の表現力を小さく制限しすぎていたのではないかと考えなおした等の作業をおこなったため、予定したよりやや遅れている。

Strategy for Future Research Activity

対象とする並行プログラム論理について特にインストラクションのリオーダリングに関して既存の知識様相論理・動的論理の手法が適用できそうというところまでは至ったので、これをフォーマルなステイトメントにまで詰めて、証明を完成させたいと考えている。

Causes of Carryover

本年度は研究発表ができるだけの研究成果がなかったためそのための支出がなかった。次年度はそれに支出したいと思っているため次年度使用額が生じた。