Optimal tableaux-based decision procedure for testing satisfiability 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), Department of Applied Mathematics and Computer Science, Technical University of Denmark [Lyngby] (DTU), University of Johannesburg (UJ), Danmarks Tekniske Universitet = Technical University of Denmark (DTU), University of Johannesburg [South Africa] (UJ) |
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: |
Theoretical computer science
Negation normal form Computer science 0102 computer and information sciences 06 humanities and the arts Alternating-time Temporal Logic 0603 philosophy ethics and religion 01 natural sciences Constructive Satisfiability TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Fragment (logic) [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] 010201 computation theory & mathematics 060302 philosophy Worst-case complexity Boolean satisfiability problem Decision model |
| Zdroj: | 7th International Joint Conference on Automated Reasoning (IJCAR 2014) 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Jul 2014, Vienna, Austria. pp.277--291, ⟨10.1007/978-3-319-08587-6_21⟩ Automated Reasoning ISBN: 9783319085869 IJCAR |
| DOI: | 10.1007/978-3-319-08587-6_21⟩ |
| Popis: | International audience; We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL+ of the full Alternating time temporal logic ATL*. The method extends in an essential way a previously developed tableaux-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 ATLP formulae can reduce the complexity of the satisfiability problem. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|