• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2021 Fiscal Year Research-status Report

効率的なωオートマトン操作法と非制限的仕様検証への応用

Research Project

Project/Area Number 18K18028
Research InstitutionTakushoku University

Principal Investigator

島川 昌也  拓殖大学, 工学部, 助教 (00749161)

Project Period (FY) 2018-04-01 – 2023-03-31
Keywordsωオートマトン / 仕様検証
Outline of Annual Research Achievements

時間論理などの数学的な言語でシステムの振る舞い(トレース)についての仕様を厳密に記述し,それを検証する形式仕様検証は,人力では見つけにくい欠陥を計算機によって自動で検出できるが,計算コストが高いという問題がある.本研究では,時間論理仕様の検証の効率化に向けて,仕様検証において基礎となるωオートマトンや無限ゲームの操作・判定の効率化手法の提案,及びそれを利用した効率的な仕様検証器の実装を行う.
2021年度は,これまでに引き続き,部分シンボリック技法による効率的な実装手法の開発に取り組んだ.通常のシンボリック技法では,オートマトン全体をひとつのBinary Decision Diagram (BDD)で表現するのに対して,部分シンボリック技法ではBDDを部分的に利用する.通常のシンボリック技法には,煩雑な手続きへの適用が難しいという問題がある一方,部分シンボリック技法は,適用可能な範囲が広いという特徴を持つ.本年度は,部分シンボリック技法には複数のバリエーションがあるため,それらについて検討を行った.具体的には,次の2種類の部分シンボリックについて検討した:(i) 各遷移にラベルされる遷移条件をひとつのBDDで表現するアプローチ,(ii) 各状態からの複数の遷移をひとつのBDDで表現するアプローチ(BDDの変種であるMtBDDを利用).また,この2種類の部分シンボリック技法のユニバーサルω木オートマトンの空判定への適用についても検討し,実際にそのパフォーマンスを実験により確認した.

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

仕様検証において基礎となるωオートマトン操作・判定の効率的な実装手法の開発に取り組み,一定の成果が得られた.それゆえ,現在までの進捗状況はおおむね順調であると判断した.

Strategy for Future Research Activity

これまでに検討した部分シンボリック技法を,ユニバーサルω木オートマトンの空判定以外の判定に適用することについて検討し,実験によりそのパフォーマンスを確認する予定である.

Causes of Carryover

(理由) 新型コロナウイルス感染症の影響で,国際会議に参加することができなかったため,次年度使用額が生じた.
(利用計画) 実験のための計算機の新調を検討している.

  • Research Products

    (1 results)

All 2021

All Journal Article (1 results) (of which Peer Reviewed: 1 results)

  • [Journal Article] Efficient Realizability Checking by Modularization of LTL Specifications2021

    • Author(s)
      Ito Sohei、Osari Kenji、Shimakawa Masaya、Hagihara Shigeki、Yonezaki Naoki
    • Journal Title

      The Computer Journal

      Volume: bxab116 Pages: bxab116

    • DOI

      10.1093/comjnl/bxab116

    • Peer Reviewed

URL: 

Published: 2022-12-28  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi