講演抄録/キーワード |
講演名 |
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 |