Model-checking first-order logic: Automata and locality

Abstract

The satisfaction problem for first-order logic, namely to decide, given a finite structure double-struck A sign and a first-order formula φ, whether or not double-struck A sign |= φ is known to be PSpace-complete. In terms of parameterized complexity, where the length of φ is taken as the parameter, the problem is AW[*]-complete and therefore not expected to be fixed-parameter tractable (FPT). Nonetheless, the problem is known to be FPT when we place some structural restrictions on double-struck A sign. For some restrictions, such as when we place a bound on the treewidth of double-struck A sign, the result is obtained as a corollary of the fact that the satisfaction problem for monadic second-order logic (MSO) is FPT in the presence of such restriction [I]. This fact is proved using automata-based methods. In other cases, such as when we bound the degree of double-struck A sign, the result is obtained using methods based on the locality of firstorder logic (see [3]) and does not extend to MSO. We survey such fixed-parameter tractability results, including the recent [2] and explore the relationship between methods based on automata, locality and decompositions. © Springer-Verlag berlin Heidelberg 2007.