Integrating hybrid logics into concurrent program logic

• Project/Area Number: 23K11051
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: Chiba Institute of Technology
• Principal Investigator: 安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
• Project Period (FY): 2023-04-01 – 2026-03-31
• Project Status: Granted (Fiscal Year 2023)
• Budget Amount: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000); Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000); Fiscal Year 2023: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
• Keywords: 並行プログラム論理 / 動的論理 / ハイブリッド論理

Outline of Research at the Start

本研究は論理学分野で最近特に研究が進んでいる時間を扱う論理（ハイブリッド論理等）を並行プログラム論理の外部論理として用いた際の有用性について調べることを目的としています。また、並行プログラム論理の外部論理に時間を扱う論理に採用することを考慮することにより導かれる並行プログラム論理の拡張、特にメモリ一貫性モデルを考慮できる論理への拡張を目指します。これにより、より実用的なプログラムを現実的な環境設定で検査できる並行プログラム論理の基礎の確立を目指します。

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

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