课题基金 / 基金详情

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

モデルチェッキング法の限界を超える新しい論理的手法によるダイナミックな実時間システムのための検証ツールの実現
使用超越模型检查方法限制的新逻辑方法实现动态实时系统的验证工具
批准号：
13224081
负责人：
岡田 光弘
金额：
$0.0万
依托单位：
Keio University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas (C)
财政年份：
2001
资助国家：
日本
项目状态：
已结题
起止时间：
2001 至 --
来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13224081/
关键词：
実時間システムモデルチェッキング形式検証線形論理論理的検証システム

项目摘要

项目成果

岡田 光弘的其他基金

相似基金

相关文献

中文摘要
翻译
点击翻译按钮获取中文摘要
英文摘要
申請者がこれまでに確立した、線形論理に基づいた(有限状態)稠密実時間並行システムの仕様・検証の形式的体系に対する、(1)証明のPSPACE決定可能性と、(2)発展的実時間システムの検証に対する適応性と,(3)(表示的意味論に対する)完全性いう3つの結果を用いて、論理的手法による実時間システム検証の理論を完成させた。特に、我々の枠組みでは、ダイナミックな変化を許す進化的、発展的実時間システムの安全性、リアクティヴ性、種々のスケジュール問題の自動検証、解析が可能である。エージェントの数が増加したり(例えば、鉄道交通網のある状況のもとで臨時列車をダイヤに組み入れたり)、時間制約が動的に変化したり(例えば、ある条件のもとで締め切り時間の延期通告が出たり)ということは、現実の実時間システムでは日常的に起こり得るが、このようなダイナミックで現実的な実時間システムに応用できる論理的検証ツールをわれわれのこれまでの理論的成果に基づいて実現するための準備研究を行った。又、我々の論理的検証系は、一部に危険な状態が生じ得ることが分っている実時間システムのなかで、安全なスケジュールを自動的に探し出したり、与えられた条件を満たすスケジュールを自動的に探しだすことを可能とする。フランス国立情報科学研究所と共同で申請者の理論の中核部分の実装試作を行ってきた。この試作された論理的検証系FATALIS Systemが来年度の日本側の上記実装研究の基盤として用いられる。
期刊论文(7)
专著(0)
科研奖励(0)
会议论文
岡田光弘: "オントロジーの哲学的・論理学的背景"人工知能学会誌. 17・2. 224-231 (2002)
冈田光宏：“本体论的哲学和逻辑背景”人工智能学会杂志17・2（2002）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
M.Okada, F.Blarqui, J-P.Jouannaud: "Inductive Data Type Systems"Theoretical Computer Science. 272. 41-68 (2002)
M.Okada、F.Blarqui、J-P.Jouannaud：“归纳数据类型系统”理论计算机科学。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
M.Okada: "La logique lineaire et les fondements de la logique intuiticniste"La rewe internationale de philosophie. (近刊). (2002)
M.Okada：“La logique lineaire et les fontements de la logique intuiticniste”La rewe Internationale de philosophie（即将出版）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
M.Okada: "A Uniform Proof for Higher Order Cut-Elimination-and Normalization Theorein"Theoretical Computer Science. (近刊). (2002)
M.Okada：“高阶削减消除和标准化理论的统一证明”理论计算机科学（即将出版）。
DOI： --
发表时间：
期刊：
影响因子： --
作者： []
通讯作者：
共 7 条
    論証・証明の哲学の深化に向けた学際的「論理の哲学」研究
    • 批准号：
      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
    海外基金