Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+
Logic in Computer Science
2015-05-28 v3
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.
Cite
@article{arxiv.1407.4645,
title = {Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+},
author = {Serenella Cerrito and Amélie David and Valentin Goranko},
journal= {arXiv preprint arXiv:1407.4645},
year = {2015}
}
Comments
45 pages