Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temoral Logic ATL+
2015 (English)In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 17, no 1, 4Article in journal (Refereed) Published
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.
Place, publisher, year, edition, pages
2015. Vol. 17, no 1, 4
Logic, satisfiability, tableaux, multi-agent systems
Research subject Mathematical Logic; Computer Science; Theoretical Philosophy
IdentifiersURN: urn:nbn:se:su:diva-123439DOI: 10.1145/2811261ISI: 000367919000004OAI: oai:DiVA.org:su-123439DiVA: diva2:874157