| 講演名 | 1995/7/7 非有界な状態空間をもつ並行システムに対する縮約状態空間の生成について 平石 邦彦, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 状態空間爆発は並行動作を許すようなシステムの検証において深刻な問題である.本稿ではプロセスが動的に生成されるような並行システムのモデルとして非有界ペトリネットを考え,その検証問題を扱う.非有界ペトリネットの状態空間は無限集合となり、そのままでは有限の手続きですべての状態を調べ尽くすことはできない.本稿では半線形集合の表現を用いることにより、有限の手続きで状態空間を表現する方法を示す.並行システムの効率的な検証方法として,デッドロック等の重要な性質を保存する縮約状態空間を構成する半順序法が提案されているが,本稿では,これらの手法が半線形集合により表現された非有界な状態空間に対しても適用可能であることを示す. |
| 抄録(英) | State space explosion is a serious problem in analyzing systems that allow concurrent occurring of events. In this paper we study efficient verification of systems in which processes are generated dynamically. Unbounded Petri nets are used for modeling such systems. Since the state space of an unbounded Petri net is infinite, it is impossible to enumerate and examine all the possible states. By using the notion of semi-linear sets, we can describe the infinite state space by finite expressions. Partial order model checking has been proposed for generating reduced state spaces that preserve some important properties such as deadlocks. We show that the partial order model checking is also applicable to unbounded state spaces represented by semi-linear sets. |
| キーワード(和) | 状態空間爆発 / 並行システム / 検証 / ペトリネット / 半線形集合 |
| キーワード(英) | state space explosion / concurrent systems / verification / Petri nets / semi-linear sets |
| 資料番号 | |
| 発行日 |
| 研究会情報 | |
| 研究会 | CST |
|---|---|
| 開催期間 | 1995/7/7(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Concurrent System Technology (CST) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 非有界な状態空間をもつ並行システムに対する縮約状態空間の生成について |
| サブタイトル（和） | |
| タイトル（英） | On Reduced State Space Generation for Concurrent Systems with Unbounded States |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 状態空間爆発 / state space explosion |
| キーワード(2)（和/英） | 並行システム / concurrent systems |
| キーワード(3)（和/英） | 検証 / verification |
| キーワード(4)（和/英） | ペトリネット / Petri nets |
| キーワード(5)（和/英） | 半線形集合 / semi-linear sets |
| 第 1 著者 氏名（和/英） | 平石 邦彦 / Kunihiko Hiraishi |
| 第 1 著者 所属（和/英） | 北陸先端科学技術大学院大学情報科学研究科 School of Information Science Japan Advanced Institute of Science and Technology (JAIST) |
| 発表年月日 | 1995/7/7 |
| 資料番号 | |
| 巻番号（vol） | vol.95 |
| 号番号（no） | 137 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |