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

2010 年度 研究成果報告書

等式付ツリーオートマトンの算術制約翻訳可能性と自動検証技術への応用に関する研究

研究課題

  • PDF
研究課題/領域番号 21700022
研究種目

若手研究(B)

配分区分補助金
研究分野 情報学基礎
研究機関独立行政法人産業技術総合研究所

研究代表者

大崎 人士  独立行政法人産業技術総合研究所, 産学官連携推進部門, 連携研究体副体長 (00356627)

研究期間 (年度) 2009 – 2010
キーワードツリーオートマトン / 書換系(rewriting systems) / 可換文法 / 算術制約
研究概要

正則ACツリーオートマトン(regular AC-tree automata)の葉言語(leaf-languages)を表現する正則可換文法(commutative regular grammar)は、線形算術制約および正数ベクトル加算系(non-negative vector-addition systems)と等価な表現力を持つ(Parikh1966他)。本研究では、正数ベクトル加算系の定義を、整数(正値、零、負値)から成る座標系上に拡張した場合、それに対応する可換文法が満たすべき代数的性質を解明する。本研究の主な成果は、可換クリーニ代数の公理系に新たな演算子i と6つの公理を導入し(i-可換クリーニ代数と呼ぶ)、i-可換正規文法は、整数ベクトル加算系と等価な表現力を持つこと、正則可換文法、線形算術制約、正数ベクトル加算系の同形関係は、整数制約上へ自然に拡張可能であることが示せたことである。

  • 研究成果

    (11件)

すべて 2011 2010 2009 その他

すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (7件) 備考 (1件) 産業財産権 (2件)

  • [雑誌論文] Checking On-The-Fly Universality And Inclusion Problems Of Visibility Pushdown Automata

    • 著者名/発表者名
      Nguyen Van Tang, 大崎人士
    • 雑誌名

      IEICE Transactions of Fundamentals

    • 査読あり
  • [学会発表] システム検証技術を社会へ-組み込みシステム産業の検証技術高度化-,招待講演2011

    • 著者名/発表者名
      大崎人士
    • 学会等名
      第8回カーエレクトロニクス研究会(主催(財)九州先端科学技術研究所)
    • 発表場所
      日本自動車会館(港区)
    • 年月日
      2011-05-20
  • [学会発表] ツリーオートマトンと計算論基礎2010

    • 著者名/発表者名
      大崎人士
    • 学会等名
      複合情報学特別講義講義第二発
    • 発表場所
      北海道大学大学院情報科学研究科(札幌市)
    • 年月日
      20101216-20101217
  • [学会発表] 可換文法-Commutative Grammar2010

    • 著者名/発表者名
      大崎人士
    • 学会等名
      記号論理と情報科学研究集会(SLACS2009)
    • 発表場所
      京都大学(京都府右京区)
    • 年月日
      2010-09-01
  • [学会発表] Equational Tree Automata, Track B (Advanced Course)2010

    • 著者名/発表者名
      大崎人士
    • 学会等名
      4th International School on Rewriting (ISR2009), RTA
    • 発表場所
      Brasilia (Brazil)
    • 年月日
      2010-06-24
  • [学会発表] システム検証技術を社会へ-組み込みシステム産業の検証技術高度化支援,基調講演2010

    • 著者名/発表者名
      大崎人士
    • 学会等名
      ソフトウエアの安全性・信頼性確保のための形式手法普及セミナー(主催三菱総合研究所・経済産業省)
    • 発表場所
      三菱総合研究所(千代田区)
    • 年月日
      2010-02-14
  • [学会発表] Collaborative Facilities for Verification : SATSUKI2009

    • 著者名/発表者名
      大崎人士, 他4名
    • 学会等名
      Workshop on Simulation Based Depelopment of Certified Embedded Systems (AIST/CVS-INRIA/LIAMA workshop)(登壇者)
    • 発表場所
      淡路夢舞台国際会議場(兵庫県淡路市)
    • 年月日
      2009-10-06
  • [学会発表] Introduction to Tree Automata, Track A (Introductory Course)2009

    • 著者名/発表者名
      大崎人士
    • 学会等名
      4th International School on Rewriting (ISR2009), RTA
    • 発表場所
      Brasilia (Brazil)
    • 年月日
      2009-06-23
  • [備考] ホームページ等

    • URL

      http://staff.asit.go.jp/hitoshi.ohsaki/

  • [産業財産権] Reactive System Safety Verification Device, Method, Program and Recording Medium Containing the Program.2009

    • 発明者名
      大崎人士、高井利憲
    • 権利者名
      独立行政法人産業技術総合研究所(大崎人士、高井利憲)
    • 産業財産権番号
      特許,No.US7503060B2
    • 取得年月日
      2009-03-10
  • [産業財産権] リアクティブ・システムの安全性検証装置、方法、プログラム及びそのプログラムを記録した記憶媒体2009

    • 発明者名
      大崎人士、高井利憲
    • 権利者名
      独立行政法人産業技術総合研究所(大崎人士、高井利憲)
    • 産業財産権番号
      特許,第4406726号
    • 取得年月日
      2009-11-20

URL: 

公開日: 2012-02-13   更新日: 2016-04-21  

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

Powered by NII kakenhi