| Presentation | 2022-03-07 Learning Assumptions for Compositional Verification of Timed Systems with Tree Queries Kotaro Niimi, Shoji Yuen, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | This paper presents an automatic assumption-learning for compositional verification of timed systems. We focus on Assume-Guarantee Reasoning (AGR), one of the compositional verification methods. AGR checks whether multiple components satisfy the property as a whole by checking whether the individual components interact correctly with the assumption without violating the desired property. Assumption learning algorithms for AGR have been proposed by Cobleigh et al. using Angluin’s L* algorithm and further extended to timed systems by Lin et al. We apply the SL* algorithm for register automata to timed systems modelled by Event-recording automata(ERA). Our assumption-learning uses tree queries to construct an observation table for the assumption ERA instead of guarded words. Our assumption includes actions to reset clocks. This enables to learn assumption ERA by a single loop and make the algorithm simpler. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Compositional verification / Timed systems / Tree query |
| Paper # | SS2021-49 |
| Date of Issue | 2022-02-28 (SS) |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2022/3/7(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Online |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | Software Science etc. |
| Chair | Takashi Kobayashi(Tokyo Inst. of Tech.) |
| Vice Chair | Kozo Okano(Shinshu Univ.) |
| Secretary | Kozo Okano(Hiroshima City Univ.) |
| Assistant | Shinpei Ogata(Shinshu Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Learning Assumptions for Compositional Verification of Timed Systems with Tree Queries |
| Sub Title (in English) | |
| Keyword(1) | Compositional verification |
| Keyword(2) | Timed systems |
| Keyword(3) | Tree query |
| 1st Author's Name | Kotaro Niimi |
| 1st Author's Affiliation | Nagoya University(Nagoya Univ) |
| 2nd Author's Name | Shoji Yuen |
| 2nd Author's Affiliation | Nagoya University(Nagoya Univ) |
| Date | 2022-03-07 |
| Paper # | SS2021-49 |
| Volume (vol) | vol.121 |
| Number (no) | SS-416 |
| Page | pp.pp.43-48(SS), |
| #Pages | 6 |
| Date of Issue | 2022-02-28 (SS) |