• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

実時間システムの形式仕様・検証のための新しい論理的方法論

研究課題

研究課題/領域番号 11878054
研究種目

萌芽的研究

配分区分補助金
研究分野 計算機科学
研究機関慶應義塾大学

研究代表者

岡田 光弘  慶應義塾大学, 文学部, 教授 (30224025)

研究期間 (年度) 1999 – 2000
研究課題ステータス 完了 (2000年度)
配分額 *注記
800千円 (直接経費: 800千円)
2000年度: 800千円 (直接経費: 800千円)
キーワード線形論理 / 実時間システム / 形式検証 / 形式仕様
研究概要

第2年次は,申請者がこれまでに確立した,線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する,証明のPSPACE決定可能性と(表示的意味論に対する)完全性という二つの定理を用いて,論理的手法による実時間システムの開発ツールを実装した.われわれのツールは次の特徴を持つ.
1.その第1は,ひとつの実時間システム全体の設計に伴う,システマティックな論理的形式仕様および,われわれの(PSPACE)決定手続きを用いた安全性・信頼性の自動検証が可能である.これは,これまでに得られた上記二つの論理的基本定理を用いることにより直接遂行できた.
2.その第2は,すでに与えられている実時間システムに新たな部分を加えたり,ある部分を変更したりするときに必要となる形式検証の問題や,二つの独立に作られた(安全性がそれぞれに対して保証されている)実時間システムを統合・総合しようとするときに必要となる形式検証の問題である.われわれの論理的な仕様・検証の枠組みは,もともと高度のモジュラー性を有しているので,このような問題に対しても本質的に上記1の方法論を応用することができた.
3.その第3は,一部に危険な状態が生じ得ることが分かっている実時間システムのなかで,ある具体的なプラン(プロセスのスケジュール)が安全であるかどうかをわれわれの論理的推論体系を用いて分析する手法の開発である.論理推論体系を(通常,定理自動証明の分野で行われているように)ボトムアップ的に用いると,論理的に証明できない命題に対しては,その反例がシステマティックに生成される.この論理推論体系の持つ基本的なメカニズムを危険な状態を示す命題に対して適用すると,その反例となるプロセススケジュール(プラン),即ち安全なプロセススケジュール(プラン)の具体例が自動的に生成・枚挙される.この手法を用いて,与えられた実時間システム内での種々のスケジューリングの問題の論理的な方法論が適用できることとなった.このようなことは,これまでの伝統的なモデルチェッキングの手法では不可能なことであった.

報告書

(2件)
  • 2000 実績報告書
  • 1999 実績報告書
  • 研究成果

    (13件)

すべて その他

すべて 文献書誌 (13件)

  • [文献書誌] F.Blanqui,J-P.Jouanraud and M.Okada: "Inductive Data Type Systems"Theoretical Computer Science. (近刊).

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] M.Kanovich,M.Okada and A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] M.Nagayama,M.Okada: "A Linear Time Characterization Theorem for Non-Commutative Linear Logic"Journal of Symbolic Logic. (近刊).

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] M.Nagayama,M.Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic"Theoretical Computer Science. (近刊).

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] 岡田光弘: "法律 人工知能(共著)"創成社出版. (2000)

    • 関連する報告書
      2000 実績報告書
  • [文献書誌] M.Okada and K.Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-801 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Okada: "A Phase-Semantic Higher Cut-elimination and Normalization Proof of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Okada and P.J.Scott: "A Note on Rewriting Theory for Uniqueness of Iteration"Journal of Theory and Applications of Categories. 6. 47-64 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] F.Banqui,J-P.Jouannaud and M.Okada: "Inductive Data Type Systems"Theoretical Computer Science. (近刊).

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] F.Banqui,J-P.Jouannaud and M.Okada: "Calculus of Inductive Construction"Proc. of Rewriting Technique and Application(RTA99),Springer-Lecture Note in Computer Science. 1631. 301-316 (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Kanovitch,M.Okada and A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] M.Okada: "Theories of Types and Proofs,second edition.Memoir of Mathematical Society of Japan vol.2"Mathematical Society of Japan. (1999)

    • 関連する報告書
      1999 実績報告書
  • [文献書誌] 岡田 光弘: "法律人工知能(共著)"創成社出版. (2000)

    • 関連する報告書
      1999 実績報告書

URL: 

公開日: 2000-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi