Author_Institution :
Dept. of Comput. Sci., Shanghai Jiaotong Univ., Shanghai, China
Abstract :
It is well-known that least fixed-point logic LFP captures the complexity class PTIME on ordered structures. The ordered conjecture claims that LFP is more expressive than first-order logic FO on every infinite class O of finite ordered structures. We present two methods which yield that LFP is more expressive than FO on various types of classes of ordered structures. The first method, the model-checking method, among others, can be applied for all such classes O of bounded cliquewidth. By the second method, the padding method, we show that for classes O of ``bounded treewidth,´´ more precisely, for classes O such that there is a bound for the treewidth of the successor structures associated with the members of O, even DTC is more expressive than FO on O, where DTC denotes the deterministic transitive closure logic, a logic that captures the complexity class L on ordered structures. Furthermore, with the padding method we get that for every infinite class of ordered structures O we have that DTC is more expressive than FO on the class of all ordered sums of pairs of structures in O. Under some complexity theoretic assumption, we prove the existence of a class O of ordered structures such that on O not only LFP is more expressive than FO, but also LFP has the expressive power of existential second-order logic. Furthermore, we characterize those classes of structures whose corresponding class of all ordered versions has bounded treewidth.
Keywords :
computational complexity; deterministic algorithms; formal logic; formal verification; trees (mathematics); bounded cliquewidth; bounded treewidth; complexity class; complexity theoretic assumption; deterministic transitive closure logic; finite ordered structure; infinite class; least fixed-point logic; model-checking method; ordered conjecture; padding method; second-order logic; Color; Complexity theory; Computer science; Electronic mail; Polynomials; Turing machines; Vocabulary; least fixed-point logic; ordered conjecture; treewidth and cliquewidth;