| 講演名 | 2009-05-22 Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築 伴 潤, 今井 敬吾, 結縁 祥治, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では,プロセス計算の操作意味を定義するときに一般的に用いられる構造操作意味定義(SOS)によって定義されるラベル付き遷移系を実現するインタプリタを書換え論理の処理系であるMaudeによって実装する.SOS規則の前件に否定を含む場合の充足性検査として,Maudeのメタレベルの探索機能を用いることで,一般的なSOSを解釈するインタプリタを構築する.さらに,SOSから導出されるラベル付き遷移系上での項に対する強双模倣等価性検証器をMaudeによって実装し,SOSによって定義される動作仕様上での等価性判定を行うツールを構築し,否定を含むSOSによって定義されるプロセス計算の例として,HennessyのTPLにおける等価性判定を示す. |
| 抄録(英) | This paper presents a general implementation by Maude of labelled transition systems specified by SOS (structural operational semantics) with negative premises. The search mechanism of the 'meta-level' in Maude eases the checking of negative premises in SOS rules. Combining a bisimulation equivalence checker with the SOS interpreter, our tool enables to show the semantic equivalence on terms specified by a general class of SOS. We illustrate the use of our tools by checking the equivalence of TPL, a process calculus proposed by Hennessy. |
| キーワード(和) | プロセス計算 / 構造操作意味定義 / Maude / 等価性検証 / 書換え論理 / メタレベル |
| キーワード(英) | Process Calculus / Structural Operational Semantics / Maude / Equivalence Checking / Rewriting Logic / Meta-Level |
| 資料番号 | SS2009-9,KBSE2009-9 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2009/5/14(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築 |
| サブタイトル（和） | |
| タイトル（英） | An SOS interpreter with negative premises and an equivalence checker by Maude |
| サブタイトル（和） | |
| キーワード(1)（和/英） | プロセス計算 / Process Calculus |
| キーワード(2)（和/英） | 構造操作意味定義 / Structural Operational Semantics |
| キーワード(3)（和/英） | Maude / Maude |
| キーワード(4)（和/英） | 等価性検証 / Equivalence Checking |
| キーワード(5)（和/英） | 書換え論理 / Rewriting Logic |
| キーワード(6)（和/英） | メタレベル / Meta-Level |
| 第 1 著者 氏名（和/英） | 伴 潤 / Jun BAN |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 2 著者 氏名（和/英） | 今井 敬吾 / Keigo IMAI |
| 第 2 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 3 著者 氏名（和/英） | 結縁 祥治 / Shoji YUEN |
| 第 3 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 発表年月日 | 2009-05-22 |
| 資料番号 | SS2009-9,KBSE2009-9 |
| 巻番号（vol） | vol.109 |
| 号番号（no） | 41 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |