Paper Info
Title
Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+.
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 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.
Year
DOI
Venue
2014
10.1007/978-3-319-08587-6_21
Lecture Notes in Artificial Intelligence
Field
DocType
Volume
Discrete mathematics,Negation normal form,Computer science,Constructive,Boolean satisfiability problem,Satisfiability,Algorithm,Theoretical computer science,Alternating-time Temporal Logic,Decision model,Worst-case complexity,Syntax
Conference
8562
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Serenella Cerrito113913.72
Amélie David 0001201.01
Valentin Goranko3124597.90