実時間システムに対する論理的仕様・検証言語の国際共同実装計画

2001 Fiscal Year Annual Research Report

• Project/Area Number: 13558031
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• Co-Investigator(Kenkyū-buntansha): 中川 中 (株)エスアールエー, ソフトウェア工学研究所, 部長 ; 田村 直之 神戸大学, 工学部, 助教授 (60207248) ; 二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
• Keywords: 実時間システム / 線形論理 / 形式検証 / 形式仕様 / 証明論

Research Abstract

第1年次は、我々の線形論理、書き換え論理の理論に基づいて、実時間並行計算システムの仕様・検証系の基礎の基礎的部分を実装した。
我々の並行計算検証系の基礎理論となる線形理論およぴ書き換え論理に基づく並行プロセス計算モデルは、これまで日本チームと米国チームとの共同研究によって確立されてきた(岡田グループと米国Mitchell-Scedrovグループによる線形理論計算モデルと二木グループとLincoln-Mesaguerグループによる書き換え計算モデルの確立)。論理的検証系設計の準備は岡田、田村グループ及びHuetのINRIAグループにより進められてきた。また、形式仕様に対する論理的方法論については、OBJ型仕様言語を対象に二木及びJouannaudにより研究されてきた。これらの研究成果を統合して、線形論理に実時間システムの形式仕様・形式検証系の中核部分を実装した。
またこの線形論理に基づく形式仕様・形式検証のわれわれのフレームワークに並行プロセスの検証ツールとして次のような反例生成系加えていくための研究を進めた。日米共同研究を通じて開発した線形論理の証明検索法によると、並行プロセスの検証の証明が与えられない場合は、(証明検索の原理と完全性定理との関係を用いて)反例が(線形論理の相意味論の上で)自動生成される。例えば、プロセスのreachabilityの検証証明に失敗する場合は、失敗した理由を示す反例がこの証明検索系により自動生成される。この理論をフランス側Huet(およびINRIA所属の協力者で、並行計算プログラムの反例分析の専門家であるF.Fage)グループの協力を得て、我々の実時間システム検証系に適用する理論を開発した。

Research Products

• [Publications] M.Okada: "A Uniform Proof for Higher Order Cut-Elimination-and Normalization Theorem"Theoretical Computer Science. (近刊). (2002)
• [Publications] M.Okada, M.Kanouchi, A.Scedrov: "Phase Semantics for Light Linear Logic and Semantic Cut-Elimination Proof"Theoretical Computer Science. (近刊). (2002)
• [Publications] M.Okada, F.Blarqui, J-P Jouannaul: "Inductive Data Type Systems"Theoretical Computer Science. 272. 41-68 (2002)
• [Publications] 岡田光弘: "オントロジーの哲学的・論理学的背景"人工知能学会誌. 17・2. 224-231 (2002)
• [Publications] M.Okada: "La logique lineaire et les fondements de la logique intuitioniste"La reme internationale de philosophie. (近刊). (2002)
• [Publications] M.Okada, M.Nagayama: "A New Correctness Criterion for the Proof-Nets of Non-Commutative Multiplicative Linear Logic"Journal of Symbolic Logic. (近刊). (2002)
• [Publications] 岡田光弘(共著): "Discover Science"Springer社. (2002)