Module checking of pushdown multi-agent systems
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2020
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915850537140224 |
|---|---|
| author | Bozzelli, Laura Murano, Aniello Peron, Adriano |
| author_facet | Bozzelli, Laura Murano, Aniello Peron, Adriano |
| contents | In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown module-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2003_04728 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Module checking of pushdown multi-agent systems Bozzelli, Laura Murano, Aniello Peron, Adriano Logic in Computer Science Formal Languages and Automata Theory Multiagent Systems In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown module-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time. |
| title | Module checking of pushdown multi-agent systems |
| topic | Logic in Computer Science Formal Languages and Automata Theory Multiagent Systems |
| url | https://arxiv.org/abs/2003.04728 |