発展的実時間システムの自動検証を可能にする新しい論理的検証理論

2001 Fiscal Year Annual Research Report

• Project/Area Number: 13878059
• Research Category: Grant-in-Aid for Exploratory Research
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部・哲学科, 教授 (30224025)
• Keywords: 実時間システム / 自動検証 / 線形論理 / 形式検証

Research Abstract

第1年次は、申請者がこれまでに確立した、線形論理に基づいた(有限状態)実時間並行システム仕様・検証の形式的体系に対する、(1)証明のPSPACE決定可能性と、(2)発展的実時間システムの検証に対する適応性と,(3)(表示的意味論に対する)完全性いう3つの結果を用いて、論理的手法による実時間システム検証の方法論を確立した。このためには、大きく分けて2つの方向性を探求した。
1.その第1は、実時間システム全体の設計に伴う、体系的で論理的な形式仕様の方法論および、実時間システムの安全性・リアクティヴ性、種々のスケジューリング問題等の自動検証の方法論の開発である。これは、これまでに得られた我々の論理的検証系に対するPSPACE決定性定理を用いることにより直接遂行した。
2.その第2は、ダイナミックな変化を許す進化的、発展的実時間システム特有の検証、解析法の開発である。エージェントの数が増加したり、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証理論をわれわれの基本定理により開発した。

Research Products

• [Publications] M.Okada: "A Uniform Proof for Higher Order Cut-Elimination- and Normalization Theorem"Theoretical Computer Science. (近刊). (2002)
• [Publications] M.Okada, M.Kanovich, A.Scedrov: "Phase Semantics for Light Linear Logic and Semantic Cut-Elimination Proof"Theoretical Computer Science. (近刊). (2002)
• [Publications] M.Okada, F.Blanqui, J-P.Jouannand: "Inductive Data Type Systems"Theoretical Computer Science. 272. 41-68 (2002)
• [Publications] 岡田光弘: "オントロジーの哲学的・論理学的背景"人工知能学会誌. 17,2. 224-231 (2002)
• [Publications] M.Okada: "La logique lineaire et les fondements de la logique intuitioniste"La revue internationale de philosophie. (近刊). (2002)
• [Publications] M.Okada, M.Nagayama: "A New Correctness Criterion for the Proof-Nets of Non-Commutative Multiplicative Linear Logic"Journal of Symbolic Logic. (近刊). (2002)
• [Publications] 岡田光弘(共著): "Discover Science"Springer社. (2002)