| 講演名 | 2015-01-27 部分観測におけるMaxSATソルバを用いたスーパバイザ合成手法 廣田 樹, 結縁 祥治, 東道 徹也, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 部分観測のもとでの離散事象システムのスーパバイザ構成アルゴリズムは指数時間であることが知られている.部分観測のもとではスーパバイザが存在する,かつその時にかぎり,制御仕様は可制御性及びノーマル性を満たす.さらに、スーパーバイザが存在しないとき部分観測に対するノーマル性を満たす最大の部分仕様が存在する.本研究では,制御仕様の可制御ノーマル性の検証問題を部分最大充足可能性問題に帰着し, MaxSATソルバを用いて最大可制御ノーマル部分仕様を導出する手法を提案する.提案手法を適用した例題を示し, MaxSATソルバによる発見的な解を示す. |
| 抄録(英) | Synthesis of the supervisor for discrete event systems under partial observation has been shown exponential. The supervisor under partial observation for a given masking exists if and only if the specification satisfies controllablity and normality with respect to the masking. Moreover, when no supervisor exists, it is known that there exists the supremal controllable sub-specification for existence of supervisors under the normality with respect to the masking. We propose a method to derive the supremal controllable and normal sub-specification using MaxSAT solvers by encoding the controllable and normal problem as the partial maximum satisfiability problem. We show that our method derives the results in practical time by some examples. |
| キーワード(和) | 離散事象システム / スーパバイザ制御理論 / 最大充足可能性問題 / MaxSATソルバ / 部分観測 |
| キーワード(英) | discrete event systems / supervisory control / MaxSAT problem / MaxSAT solvers / partial observation |
| 資料番号 | MSS2014-82,SS2014-46 |
| 発行日 |
| 研究会情報 | |
| 研究会 | MSS |
|---|---|
| 開催期間 | 2015/1/19(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Mathematical Systems Science and its applications(MSS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 部分観測におけるMaxSATソルバを用いたスーパバイザ合成手法 |
| サブタイトル（和） | |
| タイトル（英） | A supervisor synthesis by MaxSAT solvers under partial observation |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 離散事象システム / discrete event systems |
| キーワード(2)（和/英） | スーパバイザ制御理論 / supervisory control |
| キーワード(3)（和/英） | 最大充足可能性問題 / MaxSAT problem |
| キーワード(4)（和/英） | MaxSATソルバ / MaxSAT solvers |
| キーワード(5)（和/英） | 部分観測 / partial observation |
| 第 1 著者 氏名（和/英） | 廣田 樹 / Tatsuki HIROTA |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 2 著者 氏名（和/英） | 結縁 祥治 / Shoji YUEN |
| 第 2 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 3 著者 氏名（和/英） | 東道 徹也 / Tetsuya TOHDO |
| 第 3 著者 所属（和/英） | 株式会社デンソー DENSO CORPORATION |
| 発表年月日 | 2015-01-27 |
| 資料番号 | MSS2014-82,SS2014-46 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | 415 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |