Graphs Identified by Logics with Counting

ACM Transactions on Computational Logic, vol. 23, pp. 1–31

Abstract

We classify graphs and, more generally, finite relational structures that are identified by C^2 , that is, two-variable first-order logic with counting. Using this classification, we show that it can be decided in almost linear time whether a structure is identified by C^2 . Our classification implies that for every graph identified by this logic, all vertex-colored versions of it are also identified. A similar statement is true for finite relational structures. We provide constructions that solve the inversion problem for finite relational structures in linear time. By a result due to Otto, this problem has been known to be polynomial-time solvable. For graphs, we conclude that every C^2 -equivalence class contains a representative whose orbits are exactly the classes of the C^2 -partition of its vertex set and which has a single automorphism witnessing this fact. We show that such statements are not true for general k by providing examples of graphs of order linear in k which are identified by C^3 , but for which the orbit partition is strictly finer than the C^k -partition. We also construct identified graphs which have vertex-colored versions that are not identified by C^k .

Authors 3

1. Sandra Kiefer Aachen Lehrstuhl Informatik 7

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Lehrstuhl Informatik 7, Aachen, Germany

   RWTH Aachen University

2. Pascal Schweitzer Aachen

   RWTH Aachen University · University of Kaiserslautern

   Affiliation as printed

   TU Kaiserslautern, Algorithms and Complexity Group, Kaiserslautern, Germany

   RWTH Aachen University

3. Erkal Selman Aachen Lehrstuhl Informatik 7

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Lehrstuhl Informatik 7, Aachen, Germany

   RWTH Aachen University