モデルチェッキング法の限界を超える新しい論理的手法によるダイナミックな実時間システムのための検証ツールの実現

2001 Fiscal Year Annual Research Report

• Project/Area Number: 13224081
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• Keywords: 実時間システム / モデルチェッキング / 形式検証 / 線形論理 / 論理的検証システム

Research Abstract

申請者がこれまでに確立した、線形論理に基づいた(有限状態)稠密実時間並行システムの仕様・検証の形式的体系に対する、(1)証明のPSPACE決定可能性と、(2)発展的実時間システムの検証に対する適応性と,(3)(表示的意味論に対する)完全性いう3つの結果を用いて、論理的手法による実時間システム検証の理論を完成させた。特に、我々の枠組みでは、ダイナミックな変化を許す進化的、発展的実時間システムの安全性、リアクティヴ性、種々のスケジュール問題の自動検証、解析が可能である。エージェントの数が増加したり(例えば、鉄道交通網のある状況のもとで臨時列車をダイヤに組み入れたり)、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールをわれわれのこれまでの理論的成果に基づいて実現するための準備研究を行った。又、我々の論理的検証系は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、安全なスケジュールを自動的に探し出したり、与えられた条件を満たすスケジュールを自動的に探しだすことを可能とする。
フランス国立情報科学研究所と共同で申請者の理論の中核部分の実装試作を行ってきた。この試作された論理的検証系FATALIS Systemが来年度の日本側の上記実装研究の基盤として用いられる。

Research Products

• [Publications] M.Okada: "A Uniform Proof for Higher Order Cut-Elimination-and Normalization Theorein"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.Blarqui, J-P.Jouannaud: "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 intuiticniste"La rewe 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)