Tableau-Based Decision Procedures for Logics of Strategic Ability in Multiagent Systems

Valentin Goranko, Dmitry Shkatov

    Research output: Contribution to journalJournal articleResearchpeer-review

    Abstract

    We develop an incremental tableau-based decision procedure for the alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we believe that our tableaux are practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demonstrates the flexibility of the proposed procedure.
    Original languageEnglish
    JournalACM Transactions on Computational Logic
    Volume11
    Issue number1
    Pages (from-to)3
    ISSN1529-3785
    DOIs
    Publication statusPublished - 2010

    Cite this