Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+

TL;DR

This paper introduces a tableaux-based decision procedure for satisfiability testing and model synthesis in ATL+, achieving optimal worst-case complexity and enabling practical implementation for this logic fragment.

Contribution

It extends existing tableaux methods to ATL+, providing a sound, complete, and efficient approach with potential for complexity reduction through parametrizations.

Findings

Method operates in 2EXPTIME, matching the optimal complexity.

Extends previous ATL tableaux methods to ATL+ fragment.

Discusses complexity reduction via parametrizations.

Abstract

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 2EXPTIME, which is the optimal worst case complexity of the satisfiability problem for ATL+ . We also discuss how suitable parametrizations and syntactic restrictions on the class of input ATL+ formulae can reduce the complexity of the satisfiability problem.