時間を扱う論理と並行プログラム論理の合成に関する研究

• 研究課題/領域番号: 23K11051
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60050:ソフトウェア関連
• 研究機関: 千葉工業大学
• 研究代表者: 安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
• 研究期間 (年度): 2023-04-01 – 2026-03-31
• 研究課題ステータス: 交付 (2023年度)
• 配分額: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円); 2025年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円); 2024年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2023年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
• キーワード: 並行プログラム論理 / 動的論理 / ハイブリッド論理

研究開始時の研究の概要

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

研究実績の概要

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

現在までの達成度 (区分)

3: やや遅れている

理由

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

今後の研究の推進方策

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