Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
Identifiers
URN: urn:nbn:se:su:diva-123439DOI: 10.1145/2811261ISI: 000367919000004OAI: oai:DiVA.org:su-123439DiVA: diva2:874157
Available from: 2015-11-25 Created: 2015-11-25 Last updated: 2017-12-01Bibliographically approved

Open Access in DiVA

fulltext(1965 kB)30 downloads
File information
File name FULLTEXT01.pdfFile size 1965 kBChecksum SHA-512
31b5efa49978238c5e96e405ae1c616d1c8c37353b4add021e43c084751157e232a873f9598c8d5e0ae3236964daf2f52719442b5561c59215d0a0fe4bd63ffb
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: 30 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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 84 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf