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

摘要

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 ATL*. 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.