1999 Fiscal Year Annual Research Report

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

Research Project

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

Research Products
(8 results)

All Other

All Publications (8 results)

[Publications] M.Okada and K.Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-801 (1999)
[Publications] M.Okada: "A Phase-Semantic Higher Cut-elimination and Normalization Proof of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)
[Publications] 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)
[Publications] F.Banqui,J-P.Jouannaud and M.Okada: "Inductive Data Type Systems"Theoretical Computer Science. (近刊).
[Publications] 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)
[Publications] M.Kanovitch,M.Okada and A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).
[Publications] M.Okada: "Theories of Types and Proofs,second edition.Memoir of Mathematical Society of Japan vol.2"Mathematical Society of Japan. (1999)
[Publications] 岡田光弘: "法律人工知能(共著)"創成社出版. (2000)

1999 Fiscal Year Annual Research Report

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

Principal Investigator

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

Research Products

[Publications] M.Okada and K.Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-801 (1999)

[Publications] M.Okada: "A Phase-Semantic Higher Cut-elimination and Normalization Proof of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)

[Publications] 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)

[Publications] F.Banqui,J-P.Jouannaud and M.Okada: "Inductive Data Type Systems"Theoretical Computer Science. (近刊).

[Publications] 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)

[Publications] M.Kanovitch,M.Okada and A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).

[Publications] M.Okada: "Theories of Types and Proofs,second edition.Memoir of Mathematical Society of Japan vol.2"Mathematical Society of Japan. (1999)

[Publications] 岡田 光弘: "法律人工知能(共著)"創成社出版. (2000)

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

[Publications] 岡田光弘: "法律人工知能(共著)"創成社出版. (2000)