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

2002 年度 実績報告書

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

研究概要

種々の具体的な実時間有限状態システムのサンプルに対して我々の仕様、検証の方法論を適応し、方法論の検討・評価を行った。とくに、まず実時間システムの具体例(例えば、交通網自動制御システムの形式仕様とその安全性検証、実時間制約つきPhilosopher's Table等)に我々の方法論を適用し、われわれの論理的な方法論の有効性をこれまでの他の方法論と比較検討した。特に、マルチエージェントの数や時間制約が発展的に変化する並行計算システムの仕様・検証例を用いて、我々の方法論の独自性を考察した。
伝続的な方法論である、実時間オートマタ(Timed Automata)によるモデルチェッキングと呼ばれる手法(Henzinger, Alurら)による検証も(PSPACE)決定的であることがこれまでに知られている。これら伝読的モデルチェッキング法との比較も行い、われわれの新しい論理的方法論の特徴を調べた。又、これまでのオートマタを用いたモデル化の段階でしばしば生じるValidationの問題(実時間システムの設計者の最初の意図通にモデル化がなされているかどうかを問う問題)に焦点を当て、われわれの論理的形式仕様の方法論の優位性を示した。即ち、これまでのモデルチェッキングの方法は、ひとたび実時間オートマタによるモデルが与えられれば、安全性などの種々の検証は我々の新しい方法論同様にPSPACE決定手続きにより遂行できるが、モデルのValidationのテストという新たな問題が生じ、これを解決するのに困難な場合が生じることが知られている。われわれの論理的形式仕様の方法論では自然な表示的意味論(trace semantics)との間で完全性定理が成り立っており、論理的記述の意味が正確に把握されること、及びこのようなValidationの問題が生じないことを確認した。

研究成果

• [文献書誌] Mitsuhiro Okada: "A Uniform Proof for Higher Order Cut-Elimination and Normalization theorem"Theoretical Computer Science. 281. 471-498 (2002)
• [文献書誌] M.Kanovitch, Mitsuhiro Okada, A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. 294. 525-549 (2003)
• [文献書誌] K.Hasebe-M.Okada: "A Logical Veritication Method for Security Protocols Based on Linear Logic and Ban Logic"Hot-topic series. 2609号. 422-445 (2003)
• [文献書誌] 岡田 光弘, 長谷部 浩二: "線形論理によるセキュリティ・プロトコルの論理的検証法"電子情報通信学会「人工知能と知識処理」研究会報告集. 102. 49-54 (2002)
• [文献書誌] 岡田光弘: "オントロジー工学の論理的基礎III「現代のフォーマルオントロジーの動向とオントロジー工学」"人工知能. 17巻4号. 434-442 (2002)
• [文献書誌] 岡田光弘: "オントロジー工学の論理的基礎IV「オントロジー応用のための方法論の考察と展望」"人工知能. 17巻5号. 604-613 (2002)
• [文献書誌] M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security, proceedings of the International Symposium on Software Security, 2002"Springer, Hot-topic Series. (2003)