ダイナミックな実時間状態推移システムに対する線形論理を用いた形式検証

DOI

書誌事項

タイトル別名
  • Formal Verification of Dynamic Real-Time State-Transition Systems Using Linear Logic

抄録

線形論理を用いた実時間システムの安全性検証のための論理学的方法論を提案する．特にエージェントの数の増加や時間制約が動的に変化するシステムの分析に，我々の論理的方法論を応用する．自動検証により危険なプロセスの具体例が検出された時，このプロセスの一般的な時間制約条件を生成する証明論的方法を検討する．これは危険なプロセスを表す具体的な線形論理証明をパラメータ化することによってなされる．我々の検証システムの設計に当たっては，線形論理のある部分体系の決定問題に対する数学的存在定理の証明の一つを構成的証明に変換することが基本となった．もともとの証明は集合論的操作を用いた非常に非構成的な存在定理の形で得られていたが，我々はこの非構成的証明から構成的なアルゴリズムを抽出した．

収録刊行物

キーワード

詳細情報 詳細情報について

  • CRID
    1390282680501952000
  • NII論文ID
    130004638769
  • DOI
    10.11309/jssstconference.2003.0.28.0
  • ISSN
    13493515
  • データソース種別
    • JaLC
    • CiNii Articles
  • 抄録ライセンスフラグ
    使用不可

問題の指摘

ページトップへ