Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userUniversal covers, color refinement, and two-variable counting logic: Lower bounds for the depth
121
0
0.0
(
0
)
Added by
Oleg Verbitsky
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Given a connected graph $G$ and its vertex $x$, let $U_x(G)$ denote the universal cover of $G$ obtained by unfolding $G$ into a tree starting from $x$. Let $T=T(n)$ be the minimum number such that, for graphs $G$ and $H$ with at most $n$ vertices each, the isomorphism of $U_x(G)$ and $U_y(H)$ surely follows from the isomorphism of these rooted trees truncated at depth $T$. Motivated by applications in theory of distributed computing, Norris [Discrete Appl. Math. 1995] asks if $T(n)le n$. We answer this question in the negative by establishing that $T(n)=(2-o(1))n$. Our solution uses basic tools of finite model theory such as a bisimulation version of the Immerman-Lander 2-pebble counting game. The graphs $G_n$ and $H_n$ we construct to prove the lower bound for $T(n)$ also show some other tight lower bounds. Both having $n$ vertices, $G_n$ and $H_n$ can be distinguished in 2-variable counting logic only with quantifier depth $(1-o(1))n$. It follows that color refinement, the classical procedure used in isomorphism testing and other areas for computing the coarsest equitable partition of a graph, needs $(1-o(1))n$ rounds to achieve color stabilization on each of $G_n$ and $H_n$. Somewhat surprisingly, this number of rounds is not enough for color stabilization on the disjoint union of $G_n$ and $H_n$, where $(2-o(1))n$ rounds are needed.
rate research
Read More
We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of $n$-element structures that can be distinguished by a $k$-variable first-order sentence but where every such sentence requires quantifier depth at least $n^{Omega(k/log k)}$. Our trade-offs also apply to first-order counting logic, and by the known connection to the $k$-dimensional Weisfeiler--Leman algorithm imply near-optimal lower bounds on the number of refinement iterations. A key component in our proof is the hardness condensation technique recently introduced by [Razborov 16] in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the minimal quantifier depth to distinguish them in finite variable logics.
Given two structures $G$ and $H$ distinguishable in $fo k$ (first-order logic with $k$ variables), let $A^k(G,H)$ denote the minimum alternation depth of a $fo k$ formula distinguishing $G$ from $H$. Let $A^k(n)$ be the maximum value of $A^k(G,H)$ over $n$-element structures. We prove the strictness of the quantifier alternation hierarchy of $fo 2$ in a strong quantitative form, namely $A^2(n)ge n/8-2$, which is tight up to a constant factor. For each $kge2$, it holds that $A^k(n)>log_{k+1}n-2$ even over colored trees, which is also tight up to a constant factor if $kge3$. For $kge 3$ the last lower bound holds also over uncolored trees, while the alternation hierarchy of $fo 2$ collapses even over all uncolored graphs. We also show examples of colored graphs $G$ and $H$ on $n$ vertices that can be distinguished in $fo 2$ much more succinctly if the alternation number is increased just by one: while in $Sigma_{i}$ it is possible to distinguish $G$ from $H$ with bounded quantifier depth, in $Pi_{i}$ this requires quantifier depth $Omega(n^2)$. The quadratic lower bound is best possible here because, if $G$ and $H$ can be distinguished in $fo k$ with $i$ quantifier alternations, this can be done with quantifier depth $n^{2k-2}$.
It is shown that the finite satisfiability problem for two-variable logic over structures with one total preorder relation, its induced successor relation, one linear order relation and some further unary relations is EXPSPACE-complete. Actually, EXPSPACE-completeness already holds for structures that do not include the induced successor relation. As a special case, the EXPSPACE upper bound applies to two-variable logic over structures with two linear orders. A further consequence is that satisfiability of two-variable logic over data words with a linear order on positions and a linear order and successor relation on the data is decidable in EXPSPACE. As a complementing result, it is shown that over structures with two total preorder relations as well as over structures with one total preorder and two linear order relations, the finite satisfiability problem for two-variable logic is undecidable.
Term modal logics (TML) are modal logics with unboundedly many modalities, with quantification over modal indices, so that we can have formulas of the form $exists y. forall x. (Box_x P(x,y) supsetDiamond_y P(y,x))$. Like First order modal logic, TML is also notoriously undecidable, in the sense that even very simple fragments are undecidable. In this paper, we show the decidability of one interesting fragment, that of two variable TML. This is in contrast to two-variable First order modal logic, which is undecidable.
We study counting propositional logic as an extension of propositional logic with counting quantifiers. We prove that the complexity of the underlying decision problem perfectly matches the appropriate level of Wagners counting hierarchy, but also that the resulting logic admits a satisfactory proof-theoretical treatment. From the latter, a type system for a probabilistic lambda-calculus is derived in the spirit of the Curry-Howard correspondence, showing the potential of counting propositional logic as a useful tool in several fields of theoretical computer science.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
