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

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12480075
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
• Co-Investigator(Kenkyū-buntansha): 米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286) ; 林 晋 神戸大学, 工学部・情報知能工学科, 教授 (40156443) ; 小林 直樹 東京大学, 大学院・理学研究科, 専任講師 (00262155)
• Keywords: 線形論理 / 実時間システム / 形式仕様 / 形式検証

Research Abstract

線形論理を用いて並行計算システムの仕様・検証系を構築する試みはこれまでも成されてきたが、これらの成果を基にして、マルチ・エージェント並行計算実時間システムの仕様・検証系の理論を構築するとともに、我々の理論に基づく実時間システムの仕様・検証系のパイロット・インプレメンテーションを行った。
又、より本格的な実装のための研究を行った。我々の実時間システム仕様・検証系の特徴は、これまでの伝統的なモデルチェッキング法では捉えられなかった、実時間システム自身の動的変化を記述したり、そのような動的変化を伴う実時間並行計算システムに対する安全性をはじめとする種々の問題の検証を可能にした点にある.

Research Products

• [Publications] F.Blanqui,J-P.Jouannaud and M.Okada: "Inductive Data Type Systems"Theoretical Computer Science. (近刊).
• [Publications] M.Kanovich,M.Okada and A.Seedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).
• [Publications] M.Nagayawa,M.Okada: "A Linear Time Characterization Theorem for Non-Commutative Linear Logic"Journal of Symbolic Logic. (近刊).
• [Publications] M.Nagayama,M.Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic"Theoretical Computer Science. (近刊).
• [Publications] 岡田光弘: "法律人工知能(共著)"創成社出版. (2000)