Change search
ReferencesLink to record
Permanent link

Direct link
Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temoral Logic ATL+
Stockholm University, Faculty of Humanities, Department of Philosophy.ORCID iD: 0000-0002-0157-1644
2015 (English)In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 17, no 1, 4Article in journal (Refereed) Published
Abstract [en]

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
Keyword [en]
Logic, satisfiability, tableaux, multi-agent systems
National Category
Computer Science
Research subject
Mathematical Logic; Computer Science; Theoretical Philosophy
URN: urn:nbn:se:su:diva-123439DOI: 10.1145/2811261ISI: 000367919000004OAI: diva2:874157
Available from: 2015-11-25 Created: 2015-11-25 Last updated: 2016-02-16Bibliographically approved

Open Access in DiVA

fulltext(1965 kB)8 downloads
File information
File name FULLTEXT01.pdfFile size 1965 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Goranko, Valentin
By organisation
Department of Philosophy
In the same journal
ACM Transactions on Computational Logic
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 8 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 58 hits
ReferencesLink to record
Permanent link

Direct link