Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL +
| Autor: | Serenella Cerrito, Valentin Goranko, Amélie David |
|---|---|
| Přispěvatelé: | Informatique, Biologie Intégrative et Systèmes Complexes (IBISC), Université d'Évry-Val-d'Essonne (UEVE), Stockholm University |
| Rok vydání: | 2015 |
| Předmět: |
Mathematical logic
General Computer Science Computer Sciences Logic [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Alternating-time Temporal Logic tableaux Constructive Satisfiability Theoretical Computer Science Computational Mathematics Datavetenskap (datalogi) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Fragment (logic) satisfiability Temporal logic multi-agent systems Boolean satisfiability problem Decision model Algorithm Mathematics |
| Zdroj: | ACM Transactions on Computational Logic ACM Transactions on Computational Logic, Association for Computing Machinery, 2015, 17 (1), pp.Article number 4. ⟨10.1145/2811261⟩ ACM Transactions on Computational Logic, 2015, 17 (1), pp.Article number 4. ⟨10.1145/2811261⟩ |
| ISSN: | 1557-945X 1529-3785 |
| DOI: | 10.1145/2811261 |
| Popis: | We develop a sound, complete, and practically implementable tableau-based decision method for constructive satisfiability testing and model synthesis for the fragment ATL + of the full alternating-time temporal logic ALT * . The method extends in an essential way a previously developed tableau-based decision method for ATL and works in 2EXPTIME, which is the optimal worst-case complexity of the satisfiability problem for ATL + . We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL + formulas can reduce the complexity of the satisfiability problem. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|