FO Model Checking of Interval Graphs

  • Robert Ganian
  • Petr Hliněný
  • Daniel Král’
  • Jan Obdržálek
  • Jarett Schwartz
  • Jakub Teska
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7966)


We study the computational complexity of the FO model checking problem on interval graphs, i.e., intersection graphs of intervals on the real line. The main positive result is that this problem can be solved in time O(n logn) for n-vertex interval graphs with representations containing only intervals with lengths from a prescribed finite set. We complement this result by showing that the same is not true if the lengths are restricted to any set that is dense in some open subset, e.g., in the set (1, 1 + ε).


FO model checking parameterized complexity interval graph clique-width 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Courcelle, B.: The monadic second order logic of graphs I: Recognizable sets of finite graphs. Inform. and Comput. 85, 12–75 (1990)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Courcelle, B., Makowsky, J.A., Rotics, U.: Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst. 33, 125–150 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Courcelle, B., Olariu, S.: Upper bounds to the clique width of graphs. Discrete Appl. Math. 101, 77–114 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Dawar, A., Grohe, M., Kreutzer, S.: Locally excluding a minor. In: LICS 2007, pp. 270–279. IEEE Computer Society (2007)Google Scholar
  5. 5.
    Dawar, A., Kreutzer, S.: Parameterized complexity of first-order logic. ECCC TR09-131 (2009)Google Scholar
  6. 6.
    Downey, R., Fellows, M.: Parameterized complexity. Monographs in Computer Science. Springer (1999)Google Scholar
  7. 7.
    Dvořák, Z., Král’, D., Thomas, R.: Deciding first-order properties for sparse graphs. In: FOCS 2010, pp. 133–142. IEEE Computer Society (2010)Google Scholar
  8. 8.
    Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fund. Math. 49, 129–141 (1961)MathSciNetzbMATHGoogle Scholar
  9. 9.
    Fellows, M., Hermelin, D., Rosamond, F., Vialette, S.: On the parameterized complexity of multiple-interval graph problems. Theoret. Comput. Sci. 410, 53–61 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Fraïssé, R.: Sur quelques classifications des systèmes de relations. Université d’Alger, Publications Scientifiques, Série A 1, 35–182 (1954)Google Scholar
  11. 11.
    Frick, M., Grohe, M.: Deciding first-order properties of locally tree-decomposable structures. J. ACM 48, 1184–1206 (2001)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Golumbic, M., Rotics, U.: On the clique-width of some perfect graph classes. Int. J. Found. Comput. Sci. 11, 423–443 (2000)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Grohe, M., Kreutzer, S.: Methods for algorithmic meta theorems. In: Model Theoretic Methods in Finite Combinatorics Contemporary Mathematics, pp. 181–206. AMS (2011)Google Scholar
  14. 14.
    Kneis, J., Langer, A., Rossmanith, P.: Courcelle’s theorem — a game-theoretic approach. Discrete Optimization 8(4), 568–594 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  15. 15.
    Kreutzer, S.: Algorithmic meta-theorems. ECCC TR09-147 (2009)Google Scholar
  16. 16.
    Langer, A., Reidl, F., Rossmanith, P., Sikdar, S.: Evaluation of an mso-solver. In: ALENEX 2012, pp. 55–63. SIAM / Omnipress (2012)Google Scholar
  17. 17.
    Lozin, V.: From tree-width to clique-width: Excluding a unit interval graph. In: Hong, S.-H., Nagamochi, H., Fukunaga, T. (eds.) ISAAC 2008. LNCS, vol. 5369, pp. 871–882. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    Nešetřil, J., Ossona de Mendez, P.: Grad and classes with bounded expansion I. Decompositions. European J. Combin. 29, 760–776 (2008)zbMATHCrossRefGoogle Scholar
  19. 19.
    Nešetřil, J., Ossona de Mendez, P.: Grad and classes with bounded expansion II. Algorithmic aspects. European J. Combin. 29, 777–791 (2008)zbMATHGoogle Scholar
  20. 20.
    Nešetřil, J., Ossona de Mendez, P.: Grad and classes with bounded expansion III. Restricted graph homomorphism dualities. European J. Combin. 29, 1012–1024 (2008)zbMATHGoogle Scholar
  21. 21.
    Rabin, M.O.: A simple method for undecidability proofs and some applications. In: Logic, Methodology and Philosophy of Sciences, vol. 1, pp. 58–68. North-Holland (1964)Google Scholar
  22. 22.
    Seese, D.: Linear time computable problems and first-order descriptions. Math. Structures Comput. Sci. 6, 505–526 (1996)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Robert Ganian
    • 1
  • Petr Hliněný
    • 2
  • Daniel Král’
    • 3
  • Jan Obdržálek
    • 2
  • Jarett Schwartz
    • 4
  • Jakub Teska
    • 5
  1. 1.Vienna University of TechnologyAustria
  2. 2.Masaryk UniversityBrnoCzech Republic
  3. 3.University of WarwickCoventryUnited Kingdom
  4. 4.UC BerkeleyBerkeleyUnited States
  5. 5.University of West BohemiaPilsenCzech Republic

Personalised recommendations