| 講演名 | 2022-03-28 オパシティを保証するプランニングのためのシールド設計 金島 昂輝(阪大), 潮 俊光(阪大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | オパシティは hyperLTL を用いて表現される hyperproperty の一つである.トレース上の秘密と観測を考え,異なる秘密を持つが,観測が同じであるトレースが複数存在する場合はオパシティが満たされる.また,シールドはsafety な仕様を強制するために提案された手法である.シールドはシステムの出力の監視と修正を行う.本報告では,プランニング問題を対象として,2種類のオパシティを保証するシールドを構成するアルゴリズムを提案する.シールドの仕様自体を hyperLTL で記述し,QBF 問題として扱う.それを SMT ソルバーを用いて解くことでシールドの出力が計算される.2種類のオパシティに対して,シミュレーションを行い,シールドの出力を確認した. |
| 抄録(英) | Opacity is one of the hyperproperties that can be expressed using hyperLTL. Consider a secret and an observation on a trace, and if there are multiple traces with different secrets but the same observation, then the opacity is satisfied. A shield was proposed to enforce safety specifications at runtime. The shield monitors and modifies the output of the system. In this paper, we propose an algorithm for constructing a shield that guarantees two types of opacity for the planning problem. The specification of the shield itself is written in hyperLTL and converted into a QBF problem. The output of the shield is computed by solving the problem using an SMT solver. We simulated the output of the shield for two types of opacity. |
| キーワード(和) | シールド / プランニング / hyperLTLf / オパシティ |
| キーワード(英) | Shield / Planning / HyperLTLｆ / Opacity |
| 資料番号 | MSS2021-55,NLP2021-126 |
| 発行日 | 2022-03-21 (MSS, NLP) |
| 研究会情報 | |
| 研究会 | MSS / NLP |
|---|---|
| 開催期間 | 2022/3/28(から2日開催) |
| 開催地（和） | オンライン開催 |
| 開催地（英） | Online |
| テーマ（和） | MSS，NLP，一般，およびWIP（MSSのみ） |
| テーマ（英） | MSS, NLP, Work In Progress (MSS only), and etc. |
| 委員長氏名（和） | 尾崎 敦夫(阪工大) / 高坂 拓司(中京大) |
| 委員長氏名（英） | Atsuo Ozaki(Osaka Inst. of Tech.) / Takuji Kosaka(Chukyo Univ.) |
| 副委員長氏名（和） | 山口 真悟(山口大) / 常田 明夫(熊本大) |
| 副委員長氏名（英） | Shingo Yamaguchi(Yamaguchi Univ.) / Akio Tsuneda(Kumamoto Univ.) |
| 幹事氏名（和） | 小林 孝一(北大) / 劉 健全(NEC) / 松下 春奈(香川大) / 吉岡 大三郎(崇城大) |
| 幹事氏名（英） | Koichi Kobayashi(Hokkaido Univ.) / Jianquan Liui(NEC) / Haruna Matsushita(Kagawa Univ.) / Daizaburo Yoshioka(Sojo Univ.) |
| 幹事補佐氏名（和） | 白井 匡人(島根大) / 加藤 秀行(大分大) / 横井 裕一(長崎大) |
| 幹事補佐氏名（英） | Masato Shirai(Shimane Univ.) / Hideyuki Kato(Oita Univ.) / Yuichi Yokoi(Nagasaki Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Mathematical Systems Science and its Applications / Technical Committee on Nonlinear Problems |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | オパシティを保証するプランニングのためのシールド設計 |
| サブタイトル（和） | |
| タイトル（英） | Shield Synthesis for Opacity-Enforcing Planning |
| サブタイトル（和） | |
| キーワード(1)（和/英） | シールド / Shield |
| キーワード(2)（和/英） | プランニング / Planning |
| キーワード(3)（和/英） | hyperLTLf / HyperLTLｆ |
| キーワード(4)（和/英） | オパシティ / Opacity |
| 第 1 著者 氏名（和/英） | 金島 昂輝 / Koki Kanashima |
| 第 1 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ.) |
| 第 2 著者 氏名（和/英） | 潮 俊光 / Toshimitsu Ushio |
| 第 2 著者 所属（和/英） | 大阪大学(略称：阪大) Osaka University(略称：Osaka Univ.) |
| 発表年月日 | 2022-03-28 |
| 資料番号 | MSS2021-55,NLP2021-126 |
| 巻番号（vol） | vol.121 |
| 号番号（no） | MSS-443,NLP-444 |
| ページ範囲 | pp.1-6(MSS), pp.1-6(NLP), |
| ページ数 | 6 |
| 発行日 | 2022-03-21 (MSS, NLP) |