Conference paper
Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
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 parameterizations and syntactic restrictions on the class of input ATL+ formulae can reduce the complexity of the satisfiability problem.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2014 |
Pages: | 277-291 |
Proceedings: | 7th International Joint Conference on Automated ReasoningInternational Joint Conference on Automated Reasoning |
Series: | Lecture Notes in Computer Science |
ISBN: | 3319085867 , 3319085875 , 9783319085869 and 9783319085876 |
ISSN: | 03029743 |
Types: | Conference paper |
DOI: | 10.1007/978-3-319-08587-6_21 |