モデルチェッキング法の限界を超えるダイナミック実時間システムのための論理的検証法

• Project/Area Number: 16016276
• Research Category: Grant-in-Aid for Scientific Research on Priority Areas
• Allocation Type: Single-year Grants
• Review Section: Science and Engineering
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• Project Period (FY): 2005 – 2006
• Project Status: Completed (Fiscal Year 2005)
• Budget Amount: ¥5,500,000 (Direct Cost: ¥5,500,000); Fiscal Year 2005: ¥2,900,000 (Direct Cost: ¥2,900,000); Fiscal Year 2004: ¥2,600,000 (Direct Cost: ¥2,600,000)
• Keywords: 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論

Research Abstract

我々の研究の枠組は論理的推論や演繹の方法論を用いて、ロジカル・リーズニングを実時間システムの構築等の形式仕様・形式検証に取り入れようとする点に(例えば伝統的モデルチェッキング法やオートマタ理論的分析と違った)最大の特徴がある。
我々の方法論がダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析に対して有効であることを示した。また、神戸大学田村研究室グループからの協力も得て、我々の理論の実装を論理型プログラム言語上で進めた。これまでの理論的研究と実装的研究の統合も行った。
論理的形式検証の方法論を認証プロトコルの安全性検証にも応用してきた。認証プロトコルの論理的検証においても、attackersの参入や新しい認証子の発行等のようなシステムのダイナミックな変化を捉える方法論を確立することが重要である。昨年度の準備研究の成果を踏まえて、protocol logicsの論理的分析を中心として、論理的検証の方法論の具体的応用を与えた。
また、特に、認証プロトコルのagreement properties検証に関するprotocol logicの基本部分を一階述語論理上で再構成し、その完全性定理及び反例生成系を与えた。この理論の応用のための反例生成系の実装試作も行った。認証プロトコルの安全性検証に関する実時間解析の手法の研究も進めた。

Research Products

• [Journal Article] Intuitionistic phase semantics is almost classical (2006)
  • Author(s): M.Kanovich, M.Okada, K.Terui
  • Journal Title: Mathematical Structure in Computer Science (近刊)
• [Journal Article] Drug Interaction Ontology and Resource-Sensitive Logical Inferences (2006)
  • Author(s): M.Okada, Y.Sugimoto, S.Yoshikawa, A.Konagaya
  • Journal Title: Algebra, Meaning, and Computation. A Festschrift in Honor of Prof. Joseph Goguen 近刊
• [Journal Article] A Crossroad of logic, psychology and behavioral genetics : Development of "BAROCO-test" in Keio Twin-Baroco Project (2006)
  • Author(s): J.Ando, C.Shikishima, Y.Sugimoto, R.Takemura, P.Grialou, K.Hiraishi, M.Okada
  • Journal Title: Reasoning and Cognition, (Keio University Press) 近刊
• [Journal Article] Cognitive Neuroscience for Deductive Reasoning and Inhibitory Mechanism : On the Belief-Bias Effect (2006)
  • Author(s): Takeo Tsujii, Mitsuhiro Okada, Shigeru Watanabe
  • Journal Title: Reasoning and Cognition, (Keio University Press) 近刊
• [Journal Article] Completeness and Counter-Example Generations of a Basic Protocol Logic (2005)
  • Author(s): K.Hasebe, M.Okada
  • Journal Title: Electronic Notes in Computer Science, Invited Paper of the 6th International Workshop on Rule-Based Programming (RULE'05) vol.147(1) Pages: 73-92
• [Journal Article] Linear Logic and Intuitionistic Logic (2005)
  • Author(s): Mitsuhiro Okada
  • Journal Title: La revue internationale de philosophie No.230 Pages: 449-481
• [Journal Article] Completeness and Counter-Example Generations of a Basic Protocol Logic (2005)
  • Author(s): K.Hasebe, M.Okada
  • Journal Title: Electronic Notes in Theoretical Computer Science ; Proc.of RULE'05 (Invited Talk) (近刊)
• [Journal Article] Questions on Two Cognitive Models of Deductive Reasoning (2005)
  • Author(s): P.Grialou, M.Okada
  • Journal Title: In Image and Reasoning, eds.P.Grialou, G.Longo and M.Okada (近刊)
• [Journal Article] Non-monotonic Properties for Proving Correctness in a Framework of Compositional Logic (2004)
  • Author(s): K.Hasebe, M.Okada
  • Journal Title: Proc.of International Workshop Foundations of Computer Security '04 Pages: 97-113
• [Journal Article] Inferences on Honesty in Compositional Logic for Security Analysis (2004)
  • Author(s): K.Hasebe, M.Okada
  • Journal Title: Lecture Note in Computer Science ; Proc.of the International Symposium on Software Security 2003 3233 Pages: 65-86
• [Journal Article] 矛盾は矛盾か (2004)
  • Author(s): 岡田光弘
  • Journal Title: 科学哲学(日本科学哲学会) 36・2 Pages: 79-102
  • NAID: 130003640593
• [Book] Towards New Logic and Semantics : Franco-Japanese Collaborative Lectures on Philosophy of Logic (2006)
  • Author(s): Mitsuhiro Okada, Jocelyn Benoist, Jean-Yves. Girard
  • Publisher: Keio University Press
• [Book] Image and Reasoning (2005)
  • Author(s): P.Grialou, G.Longo, M.Okada (Editors)
  • Publisher: Keio University Press(近刊)