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

一种新的逻辑验证理论，可实现进化实时系统的自动验证

• 批准号: 13878059
• 负责人: 岡田 光弘
• 金额: $ 1.28万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Exploratory Research
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2002
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-13878059/
• 关键词: 線形論理; 形式仕様; 形式検証; 実時間システム; 自動検証

本年度は、第1年次に開発した論理的理論を基にした仕様、検証の有効性を確かめ、仕様、検証の新しい論理的方法論を開発した。とくに、まず実時間システムの研究分野でベンチマークとして使われている代表的な実時間システムの具体例を発展的システムの例に変形し、これに我々の方法論を適用し、われわれの論理的な方法論とこれまでの他の方法論とを比較した。(例えば、今までの静的な交通網モデルを、新たに交通網が複雑化したり、電車の本数が変化したり、列車ダイヤの改定や時間制約の変化が起こったりする進化的モデルに作り変えて検討した。)とくに、これまでのPVS言語やTLA言語などで代表されるような、伝統的な述語論理に基づいた論理的手法では、述語論理の表現力を用いて形式仕様が可能であるが、これらPVS言語やTLA言語の(および、その他の述語論理に基づく)枠組では、一般に証明可能性問題が非決定的であるため、形式的検証を体系的に遂行することができなかった。そこで彼らは、この言語使用者の責任において、与えられた形式仕様に特有な種々のInvariant Propertiesを見つけだし、それをもとに多重の数学的帰納法を適用して、検証の論理的証明を構成する、というアドホックな方法を採用していた。しかし現実の問題として、少し規模が大きな実時間システムを設計しようとすると、このような適当なInvariant Propertiesを一般の設計者自身が自分の責任で見いだすことは不可能であるのが実情である。これに対して、我々の線形論理に基づいた論理体系の枠組みは(PSPACE)決定可能であるので、仕様された実時間システムの安全性検証の証明構成(または危険性の証明構成)が自動的に遂行できる。この違いを具体的な例を用いて分析した。

This year marks the first time that the theoretical basis of logic, the validity of evidence, and the methodology of new logic have been developed. The methodology of this study is applicable to the logical methodology of this study and the methodology of this study is comparable to that of other studies. (For example, today's quiet traffic network, the new traffic network, the number of trams, the train schedule, the time constraints, the evolution of the traffic network, etc.) PVS speech and TLA speech represent the basic logic of traditional predicate logic, the expressive force of predicate logic, the form of expression, the possibility of PVS speech and TLA speech (basic logic of other predicate logic), the general problem of proof possibility, the non-decision, the form of proof system. The responsibility of the speech user, the special kind of Invariant Properties, the application of multiple mathematical methods, the proof of logic, the adoption of methods, and the use of methods. The design of the problem is not possible. The design of the problem is not possible. The design of the problem is impossible. In this case, the linear logic of the logic system (PSPACE) determines the probability of occurrence, the time of occurrence, and the proof structure of the security model (proof structure of risk). This is a concrete example of how to use it.

项目成果

M.Okada, M.Kanovich, A.Scedrov: "Phase Semantics for Light Linear Logic and Semantic Cut-Elimination Proof"Theoretical Computer Science. (近刊). (2002)

M.Okada、M.Kanovich、A.Scedrov：“轻线性逻辑的相位语义和语义剪切消除证明”理论计算机科学（即将出版）。

岡田光弘: "オントロジーの哲学的・論理学的背景"人工知能学会誌. 17・2. 224-231 (2002)

冈田光宏：“本体论的哲学和逻辑背景”人工智能学会杂志17・2（2002）。

岡田光弘: "オントロジー工学の論理的基礎IV「オントロジー応用のための方法論の考察と展望」"人工知能. 17巻5号. 604-613 (2002)

Mitsuhiro Okada：“本体工程的逻辑基础 IV“本体应用方法论的考虑和展望”，第 17 卷，第 5 期。604-613 (2002)

岡田 光弘, 長谷部 浩二: "線形論理によるセキュリティ・プロトコルの論理的検証法"電子情報通信学会「人工知能と知識処理」研究会報告集. 102. 49-54 (2002)

Mitsuhiro Okada、Koji Hasebe：“使用线性逻辑的安全协议的逻辑验证方法” IEICE“人工智能和知识处理”研究组报告 102. 49-54 (2002)

M.Okada: "La logique lineaire et les fondements de la logique intuitioniste"La revue internationale de philosophie. (近刊). (2002)

M.Okada：“La logique lineaire et les fontements de la logique intuitioniste”《国际哲学评论》（即将出版）。