文献

J-GLOBAL ID：201202243431614240   整理番号：12A1583729

複数の計算モデルをサポートするモデル検査器の実現

著者 (3件)： 目黒学 (早稲田大 理工) ,  谷口直輝 (早稲田大 理工) ,  上田和紀 (早稲田大 理工学術院)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 29th  ページ： ROMBUNNO.6A-4  発行年： 2012年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： LMNtalは階層グラフの書き換えによって計算をすすめる言語であり,実行時処理系は並列LTLモデル検査器を備えている。これまでにλ計算をはじめ,Petri Net,Ambient計算,CHR,MSR,最適化問題やリアルタイムシステムなどさまざまなモデルをエンコードし検証してきた。近年では新たなデータ構造の導入による階層ハイパーグラフ書き換え言語への拡張を行いさらに表現力が向上した。本研究ではより統合的に計算モデルを扱うため,階層ハイパーグラフの状態空間構築処理の設計・実装を行うとともに,計算モデルを統合したmeta-calculusであるBigraphをエンコードする手法について検討する。本論文ではBigraphはLMNtalによって構造の大半が表現可能で,拡張によりその機能全般をエンコード可能であることを論じる。そして拡張されたLMNtalによって複数の計算モデルをサポートする枠組みについて解説する。(著者抄録)

シソーラス用語： *モデル検査 ,  *超グラフ ,  計算モデル ,  符号化 ,  階層構造 ,  データ構造 ,  項書換え系 ,  空間 ,  実装設計 ,  システム設計
準シソーラス用語： *階層ハイパーグラフ ,  状態空間

分類 (2件)： 計算理論  (JB02000A) ,  グラフ理論基礎  (IA02020S)

タイトルに関連する用語 (2件)： 計算モデル ,  モデル検査