ATLsc with partial observation
Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-09-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1509.07208v1 |
| _version_ | 1811230791091355648 |
|---|---|
| author | François Laroussinie Nicolas Markey Arnaud Sangnier |
| author_facet | François Laroussinie Nicolas Markey Arnaud Sangnier |
| author_sort | François Laroussinie |
| collection | DOAJ |
| description | Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model-checking problem, even for very expressive logics such as ATLsc. |
| first_indexed | 2024-04-12T10:34:13Z |
| format | Article |
| id | doaj.art-eb7f55dc24ec452ab88e7bc47b39d533 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T10:34:13Z |
| publishDate | 2015-09-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-eb7f55dc24ec452ab88e7bc47b39d5332022-12-22T03:36:46ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-09-01193Proc. GandALF 2015435710.4204/EPTCS.193.4:12ATLsc with partial observationFrançois Laroussinie0Nicolas Markey1Arnaud Sangnier2 LIAFA, Univ. Paris Diderot and CNRS, France LSV, ENS Cachan and CNRS, France LIAFA, Univ. Paris Diderot and CNRS, France Alternating-time temporal logic with strategy contexts (ATLsc) is a powerful formalism for expressing properties of multi-agent systems: it extends CTL with strategy quantifiers, offering a convenient way of expressing both collaboration and antagonism between several agents. Incomplete observation of the state space is a desirable feature in such a framework, but it quickly leads to undecidable verification problems. In this paper, we prove that uniform incomplete observation (where all players have the same observation) preserves decidability of the model-checking problem, even for very expressive logics such as ATLsc.http://arxiv.org/pdf/1509.07208v1 |
| spellingShingle | François Laroussinie Nicolas Markey Arnaud Sangnier ATLsc with partial observation Electronic Proceedings in Theoretical Computer Science |
| title | ATLsc with partial observation |
| title_full | ATLsc with partial observation |
| title_fullStr | ATLsc with partial observation |
| title_full_unstemmed | ATLsc with partial observation |
| title_short | ATLsc with partial observation |
| title_sort | atlsc with partial observation |
| url | http://arxiv.org/pdf/1509.07208v1 |
| work_keys_str_mv | AT francoislaroussinie atlscwithpartialobservation AT nicolasmarkey atlscwithpartialobservation AT arnaudsangnier atlscwithpartialobservation |