線形論理を用いた並行計算システム及び実時間システムの形式仕様・形式検証の理論

2001 年度 実績報告書

• 研究課題/領域番号: 12480075
• 研究機関: 慶應義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• 研究分担者: 米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286) ; 小林 直樹 東京工業大学, 大学院・情報理工学研究科, 助教授 (00262155)
• キーワード: 線形論理 / 定時間システム / 形式仕様 / 形式検証

研究概要

平成13年度(第2年次)は、第1年次に確立した、線形論理に基づいた(有限状態)並行計算システムの仕様・検証の形式的体系とこれまでの我々の準備研究で得られた線形論理による実時間システムの新しい検証理論とを組み合わせて、実時間並行計算システムの仕様・検証の形式体系を確立した。このためには、岡田-Scedrov-Mitchellの共同研究の成果を軸にして、大きく分けて2つの方向性を探求した。
1.ひとつの実時間システム全体の設計に伴う、自然言語で書かれた仕様から(線形)論理的形式仕様へのシステマティックな自動翻訳法を与えた。これはこれまでの伝統的なモデルチェッキングの手法にはなかったわれわれの論理的方法論の特徴の1つである。また、この線形論理上に翻訳された仕様に対してわれわれの(PSPACE)決定手続きを用いた安全性・信頼性の自動検証の方法論を確立した。
2.その第2は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析する手法の開発である。論理推論体系を(通常、定理自動証明の分野で行われているように)ボトムアッブ的に用いると、論理的に証明できない命題に対しては、その反例がシステマティックに生成される。この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると、その反例となるプロセススケジュール(プラン)、即ち安全なプロセススケジュール(プラン)の具体例が自動的に生成・枚挙される手続きが得られるのである。この手法を用いて、与えられた実時間システム内での種々のプラニングの問題の論理的な手法を研究した。

研究成果

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