课题基金 / 基金详情

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

発展的実時間システムの自動検証を可能にする新しい論理的検証理論
一种新的逻辑验证理论，可实现进化实时系统的自动验证
批准号：
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)決定可能であるので、仕様された実時間システムの安全性検証の証明構成(または危険性の証明構成)が自動的に遂行できる。この違いを具体的な例を用いて分析した。
期刊论文(17)
专著(0)
科研奖励(0)
会议论文
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：“轻线性逻辑的相位语义和语义剪切消除证明”理论计算机科学（即将出版）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
岡田光弘: "オントロジーの哲学的・論理学的背景"人工知能学会誌. 17・2. 224-231 (2002)
冈田光宏：“本体论的哲学和逻辑背景”人工智能学会杂志17・2（2002）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
岡田光弘: "オントロジー工学の論理的基礎IV「オントロジー応用のための方法論の考察と展望」"人工知能. 17巻5号. 604-613 (2002)
Mitsuhiro Okada：“本体工程的逻辑基础 IV“本体应用方法论的考虑和展望”，第 17 卷，第 5 期。604-613 (2002)
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
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”《国际哲学评论》（即将出版）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
共 14 条
    論証・証明の哲学の深化に向けた学際的「論理の哲学」研究
    • 批准号：
      23K20416
    • 项目类别：
      Grant-in-Aid for Scientific Research (B)
    • 资助金额：
      $3.24万
    • 财政年份：
      2024
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    On information presentation methods for easier decison making: Studies on multi-attribute decision making
    • 批准号：
      21K18339
    • 项目类别：
      Grant-in-Aid for Challenging Research (Exploratory)
    • 资助金额：
      $4.08万
    • 财政年份：
      2021
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    Interdisciplinary studies on philosophy of logic: Toward the development of philosophy of proof and demonstration
    • 批准号：
      21H00467
    • 项目类别：
      Grant-in-Aid for Scientific Research (B)
    • 资助金额：
      $8.49万
    • 财政年份：
      2021
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    Study on "Disagreement" in logic
    • 批准号：
      19KK0006
    • 项目类别：
      Fund for the Promotion of Joint International Research (Fostering Joint International Research (B))
    • 资助金额：
      $7.49万
    • 财政年份：
      2019
    • 负责人：
      岡田 光弘
    • 依托单位：
      Keio University
    海外基金