• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2021 年度 実績報告書

データ値付きプログラムに対するモデル検査理論の構築と実装

研究課題

研究課題/領域番号 21J14332
研究機関名古屋大学

研究代表者

仙田 涼摩  名古屋大学, 情報学研究科, 特別研究員(DC2)

研究期間 (年度) 2021-04-28 – 2023-03-31
キーワード形式言語理論 / ソフトウェア工学 / ソフトウェア合成 / レジスタ付き計算モデル
研究実績の概要

プログラムに含まれるバグを無くしてシステムの安全性を確保する手法として、システムに対する入力/出力の制約を記述した仕様書からプログラムを自動生成する「リアクティブ合成」というアプローチがよく知られている。本分野において、「ある計算モデルAによって表現される仕様について、これを満たす実装 Tを構築できるか?」という問題を合成可能性問題と呼ぶ。この問題は、仕様×実装の組が有限オートマトン(NFA)×有限文字列変換器(FT)の場合に決定可能であることが示されているほか、NFAとFTに対してデータ値を扱えるよう拡張したレジスタオートマトン(RA)とレジスタ付き文字列変換器(RT)を仕様、実装とする場合についても考察がなされているが、仕様と実装がプッシュダウンモデルの場合については十分な研究がなされていなかった。
本研究にて、我々はプッシュダウンオートマトン(PDA)×プッシュダウン文字列変換器(PDT)に関する合成可能性問題が、PDAが決定性の場合は指数時間可解、非決定性の場合は決定不能であることを証明した。加えて、PDA、PDTにレジスタを付加して拡張したRPDA、RPDTについても合成可能性問題を考察し、問題が二重指数時間可解となるような制約(visibly決定性)を提案した。また、具体的にvisibly決定性RPDAで表現される仕様を満たす実装であるRPDTが存在する場合に、そのRPDTを構成するアルゴリズムを示した。一般的なプログラムはデータ値、スタック等を含んでいることが多く、これらを扱えるモデルに関する合成可能性問題について考察した本研究の成果を用いることで、より実用的な表現を仕様に許すことが可能になる。

現在までの達成度 (段落)

翌年度、交付申請を辞退するため、記入しない。

今後の研究の推進方策

翌年度、交付申請を辞退するため、記入しない。

  • 研究成果

    (2件)

すべて 2021

すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (1件) (うち国際学会 1件)

  • [雑誌論文] LTL Model Checking for Register Pushdown Systems2021

    • 著者名/発表者名
      SENDA Ryoma、TAKATA Yoshiaki、SEKI Hiroyuki
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: E104.D ページ: 2131~2144

    • DOI

      10.1587/transinf.2020EDP7265

    • 査読あり
  • [学会発表] Reactive Synthesis from Visibly Register Pushdown Automata2021

    • 著者名/発表者名
      SENDA Ryoma
    • 学会等名
      18th International Colloquium on Theoretical Aspects of Computing (ICTAC 2021)
    • 国際学会

URL: 

公開日: 2022-12-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi