Presentation | 2022-03-28 Shield Synthesis for Opacity-Enforcing Planning Koki Kanashima, Toshimitsu Ushio, |
---|---|
PDF Download Page | PDF download Page Link |
Abstract(in Japanese) | (See Japanese page) |
Abstract(in English) | 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. |
Keyword(in Japanese) | (See Japanese page) |
Keyword(in English) | Shield / Planning / HyperLTLf / Opacity |
Paper # | MSS2021-55,NLP2021-126 |
Date of Issue | 2022-03-21 (MSS, NLP) |
Conference Information | |
Committee | MSS / NLP |
---|---|
Conference Date | 2022/3/28(2days) |
Place (in Japanese) | (See Japanese page) |
Place (in English) | Online |
Topics (in Japanese) | (See Japanese page) |
Topics (in English) | MSS, NLP, Work In Progress (MSS only), and etc. |
Chair | Atsuo Ozaki(Osaka Inst. of Tech.) / Takuji Kosaka(Chukyo Univ.) |
Vice Chair | Shingo Yamaguchi(Yamaguchi Univ.) / Akio Tsuneda(Kumamoto Univ.) |
Secretary | Shingo Yamaguchi(Hokkaido Univ.) / Akio Tsuneda(NEC) |
Assistant | Masato Shirai(Shimane Univ.) / Hideyuki Kato(Oita Univ.) / Yuichi Yokoi(Nagasaki Univ.) |
Paper Information | |
Registration To | Technical Committee on Mathematical Systems Science and its Applications / Technical Committee on Nonlinear Problems |
---|---|
Language | JPN |
Title (in Japanese) | (See Japanese page) |
Sub Title (in Japanese) | (See Japanese page) |
Title (in English) | Shield Synthesis for Opacity-Enforcing Planning |
Sub Title (in English) | |
Keyword(1) | Shield |
Keyword(2) | Planning |
Keyword(3) | HyperLTLf |
Keyword(4) | Opacity |
1st Author's Name | Koki Kanashima |
1st Author's Affiliation | Osaka University(Osaka Univ.) |
2nd Author's Name | Toshimitsu Ushio |
2nd Author's Affiliation | Osaka University(Osaka Univ.) |
Date | 2022-03-28 |
Paper # | MSS2021-55,NLP2021-126 |
Volume (vol) | vol.121 |
Number (no) | MSS-443,NLP-444 |
Page | pp.pp.1-6(MSS), pp.1-6(NLP), |
#Pages | 6 |
Date of Issue | 2022-03-21 (MSS, NLP) |