Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL + | Zendy

Serenella Cerrito | Zendy; Amélie David | Zendy; Valentin Goranko | Zendy

Open Access

Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL ⁺

Author(s) -

Serenella Cerrito,

Amélie David,

Valentin Goranko

Publication year - 2015

Publication title -

acm transactions on computational logic

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.593

H-Index - 52

eISSN - 1557-945X

pISSN - 1529-3785

DOI - 10.1145/2811261

Subject(s) - satisfiability , constructive , temporal logic , boolean satisfiability problem , fragment (logic) , mathematics , class (philosophy) , time complexity , model checking , decision problem , algorithm , theoretical computer science , discrete mathematics , computer science , programming language , artificial intelligence , process (computing)

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research