We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL~+ of the full Alternating time temporal logic ATL~*. The method extends in an essential way a previously developed tableaux-based decision method for ATL and works in 2EXP-TIME, 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~+ formulae can reduce the complexity of the satisfiability problem.
展开▼
