| 講演抄録/キーワード |
| 講演名 |
2015-03-09 09:55
環境許容性のあるリアクティブシステム合成法 ○上野篤史・冨田 尭・島川昌也・萩原茂樹・米崎直樹(東工大) SS2014-56 |
| 抄録 |
(和) |
形式的に記述された仕様からリアクティブシステム(RS)を自動合成する手法では,仕様$varphi_{sys}$を満たす振る舞いをするRSが制約$varphi_{env}$に従う環境からの入力を想定する場合,$varphi_{env}tovarphi_{sys}$の形で仕様が記述される.この仕様からは,環境から$varphi_{env}$を満たさない想定外の入力に対してどのような振る舞いをしても良いシステムが合成されうる.
しかし,現実世界での安全性を考えた場合は,想定外の入力に対しても,$varphi_{sys}$をできるだけ満たすような環境許容性のあるRSが合成されることが望ましい.
本稿ではこのような合成手法を提案する.
一般的なRSの合成手法では,仕様の実現の集合である勝利領域から任意の戦略を選び,RSとして合成するが,本手法では,$varphi_{sys}$をできるだけ満たす振る舞いに利得を割り当てた平均利得ゲームを構築し,平均利得ゲームの最適解をRSとして合成する. |
| (英) |
On the synthesis of reactive system (RS), if we assume some behavior property on an environment, specifications must include the environmental constraint in their conditional part.
Generally, the behavior of a synthesized RS from such specification tend to satisfy the specification part only for the case where environmental behavior follows the conditional part, however, in the real world setting it is desirable that the behavior of the RS satisfies the specification part, even in the case of unexpected environmental behavior.
In this paper we discuss reactive system synthesis method with tolerance for such a case. |
| キーワード |
(和) |
形式手法 / リアクティブシステム合成 / 平均利得 / 線形時相論理 / / / / |
| (英) |
formal methods / reactive system / synthesis / tolerance of unintended behavior / / / / |
| 文献情報 |
信学技報, vol. 114, no. 510, SS2014-56, pp. 7-12, 2015年3月. |
| 資料番号 |
SS2014-56 |
| 発行日 |
2015-03-02 (SS) |
| ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
| PDFダウンロード |
SS2014-56 |
| 研究会情報 |
| 研究会 |
SS |
| 開催期間 |
2015-03-09 - 2015-03-10 |
| 開催地(和) |
沖縄県青年会館 |
| 開催地(英) |
OKINAWAKEN SEINENKAIKAN |
| テーマ(和) |
一般 |
| テーマ(英) |
|
| 講演論文情報の詳細 |
| 申込み研究会 |
SS |
| 会議コード |
2015-03-SS |
| 本文の言語 |
日本語 |
| タイトル(和) |
環境許容性のあるリアクティブシステム合成法 |
| サブタイトル(和) |
|
| タイトル(英) |
Reactive System Synthesis with Tolerance for Unexpected Environmental Behavior |
| サブタイトル(英) |
|
| キーワード(1)(和/英) |
形式手法 / formal methods |
| キーワード(2)(和/英) |
リアクティブシステム合成 / reactive system |
| キーワード(3)(和/英) |
平均利得 / synthesis |
| キーワード(4)(和/英) |
線形時相論理 / tolerance of unintended behavior |
| キーワード(5)(和/英) |
/ |
| キーワード(6)(和/英) |
/ |
| キーワード(7)(和/英) |
/ |
| キーワード(8)(和/英) |
/ |
| 第1著者 氏名(和/英/ヨミ) |
上野 篤史 / Atsushi Ueno / ウエノ アツシ |
| 第1著者 所属(和/英) |
東京工業大学 (略称: 東工大)
Tokyo Institute of Technology (略称: Tokyo Tech) |
| 第2著者 氏名(和/英/ヨミ) |
冨田 尭 / Takashi Tomita / トミタ タカシ |
| 第2著者 所属(和/英) |
東京工業大学 (略称: 東工大)
Tokyo Institute of Technology (略称: Tokyo Tech) |
| 第3著者 氏名(和/英/ヨミ) |
島川 昌也 / Masaya Shimakawa / シマカワ マサヤ |
| 第3著者 所属(和/英) |
東京工業大学 (略称: 東工大)
Tokyo Institute of Technology (略称: Tokyo Tech) |
| 第4著者 氏名(和/英/ヨミ) |
萩原 茂樹 / Shigeki Hagihara / ハギハラ シゲキ |
| 第4著者 所属(和/英) |
東京工業大学 (略称: 東工大)
Tokyo Institute of Technology (略称: Tokyo Tech) |
| 第5著者 氏名(和/英/ヨミ) |
米崎 直樹 / Naoki Yonezaki / ヨネザキ ナオキ |
| 第5著者 所属(和/英) |
東京工業大学 (略称: 東工大)
Tokyo Institute of Technology (略称: Tokyo Tech) |
| 第6著者 氏名(和/英/ヨミ) |
/ / |
| 第6著者 所属(和/英) |
(略称: )
(略称: ) |
| 第7著者 氏名(和/英/ヨミ) |
/ / |
| 第7著者 所属(和/英) |
(略称: )
(略称: ) |
| 第8著者 氏名(和/英/ヨミ) |
/ / |
| 第8著者 所属(和/英) |
(略称: )
(略称: ) |
| 第9著者 氏名(和/英/ヨミ) |
/ / |
| 第9著者 所属(和/英) |
(略称: )
(略称: ) |
| 第10著者 氏名(和/英/ヨミ) |
/ / |
| 第10著者 所属(和/英) |
(略称: )
(略称: ) |
| 第11著者 氏名(和/英/ヨミ) |
/ / |
| 第11著者 所属(和/英) |
(略称: )
(略称: ) |
| 第12著者 氏名(和/英/ヨミ) |
/ / |
| 第12著者 所属(和/英) |
(略称: )
(略称: ) |
| 第13著者 氏名(和/英/ヨミ) |
/ / |
| 第13著者 所属(和/英) |
(略称: )
(略称: ) |
| 第14著者 氏名(和/英/ヨミ) |
/ / |
| 第14著者 所属(和/英) |
(略称: )
(略称: ) |
| 第15著者 氏名(和/英/ヨミ) |
/ / |
| 第15著者 所属(和/英) |
(略称: )
(略称: ) |
| 第16著者 氏名(和/英/ヨミ) |
/ / |
| 第16著者 所属(和/英) |
(略称: )
(略称: ) |
| 第17著者 氏名(和/英/ヨミ) |
/ / |
| 第17著者 所属(和/英) |
(略称: )
(略称: ) |
| 第18著者 氏名(和/英/ヨミ) |
/ / |
| 第18著者 所属(和/英) |
(略称: )
(略称: ) |
| 第19著者 氏名(和/英/ヨミ) |
/ / |
| 第19著者 所属(和/英) |
(略称: )
(略称: ) |
| 第20著者 氏名(和/英/ヨミ) |
/ / |
| 第20著者 所属(和/英) |
(略称: )
(略称: ) |
| 第21著者 氏名(和/英/ヨミ) |
/ / |
| 第21著者 所属(和/英) |
(略称: )
(略称: ) |
| 第22著者 氏名(和/英/ヨミ) |
/ / |
| 第22著者 所属(和/英) |
(略称: )
(略称: ) |
| 第23著者 氏名(和/英/ヨミ) |
/ / |
| 第23著者 所属(和/英) |
(略称: )
(略称: ) |
| 第24著者 氏名(和/英/ヨミ) |
/ / |
| 第24著者 所属(和/英) |
(略称: )
(略称: ) |
| 第25著者 氏名(和/英/ヨミ) |
/ / |
| 第25著者 所属(和/英) |
(略称: )
(略称: ) |
| 第26著者 氏名(和/英/ヨミ) |
/ / |
| 第26著者 所属(和/英) |
(略称: )
(略称: ) |
| 第27著者 氏名(和/英/ヨミ) |
/ / |
| 第27著者 所属(和/英) |
(略称: )
(略称: ) |
| 第28著者 氏名(和/英/ヨミ) |
/ / |
| 第28著者 所属(和/英) |
(略称: )
(略称: ) |
| 第29著者 氏名(和/英/ヨミ) |
/ / |
| 第29著者 所属(和/英) |
(略称: )
(略称: ) |
| 第30著者 氏名(和/英/ヨミ) |
/ / |
| 第30著者 所属(和/英) |
(略称: )
(略称: ) |
| 第31著者 氏名(和/英/ヨミ) |
/ / |
| 第31著者 所属(和/英) |
(略称: )
(略称: ) |
| 第32著者 氏名(和/英/ヨミ) |
/ / |
| 第32著者 所属(和/英) |
(略称: )
(略称: ) |
| 第33著者 氏名(和/英/ヨミ) |
/ / |
| 第33著者 所属(和/英) |
(略称: )
(略称: ) |
| 第34著者 氏名(和/英/ヨミ) |
/ / |
| 第34著者 所属(和/英) |
(略称: )
(略称: ) |
| 第35著者 氏名(和/英/ヨミ) |
/ / |
| 第35著者 所属(和/英) |
(略称: )
(略称: ) |
| 第36著者 氏名(和/英/ヨミ) |
/ / |
| 第36著者 所属(和/英) |
(略称: )
(略称: ) |
| 講演者 |
第1著者 |
| 発表日時 |
2015-03-09 09:55:00 |
| 発表時間 |
25分 |
| 申込先研究会 |
SS |
| 資料番号 |
SS2014-56 |
| 巻番号(vol) |
vol.114 |
| 号番号(no) |
no.510 |
| ページ範囲 |
pp.7-12 |
| ページ数 |
6 |
| 発行日 |
2015-03-02 (SS) |