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

Valentin Goranko, Dmitry Shkatov

    Research output: Contribution to journalJournal articleResearchpeer-review


    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
    Issue number1
    Pages (from-to)3
    Publication statusPublished - 2010

    Cite this