Abstract
For first-order logic model checking on monotone graph classes the borderline between tractable and intractable is well charted: it is tractable on all nowhere dense classes of graphs, and this is essentially the limit. In contrast to this, there are few results concerning the tractability of model checking on general, i.e. not necessarily monotone, graph classes.
We show that model checking for first-order logic on map graphs is fixed-parameter tractable, when parameterised by the size of the input formula. Map graphs are a geometrically defined class of graphs similar to planar graphs, but here each vertex of a graph is drawn homeomorphic to a closed disk in the plane in such a way that two vertices are adjacent if, and only if, the corresponding disks intersect. Map graphs may contain arbitrarily large cliques, and are not closed under edge removal.
Our algorithm works by efficiently transforming a given map graph into a nowhere dense graph in which the original graph is first-order interpretable. As a by-product of this technique we also obtain a model checking algorithm for FO on squares of trees.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Elements of V are referred to as nations by Chen et al.
References
Chen, Z.Z., Grigni, M., Papadimitriou, C.H.: Map graphs. J. ACM 49(2), 127–138 (2002)
Courcelle, B.: Graph rewriting: an algebraic and logic approach. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. 2, pp. 194–242. Elsevier, Amsterdam (1990)
Courcelle, B., Makowsky, J., Rotics, U.: Linear time solvable optimization problems on graphs of bounded clique-width. Theory Comput. Syst. 33(2), 125–150 (2000)
Dawar, A., Grohe, M., Kreutzer, S.: Locally excluding a minor. In: Logic in Computer Science (LICS), pp. 270–279 (2007)
Diestel, R.: Graph Theory. GTM, vol. 173, 4th edn. Springer, Heidelberg (2012)
Dvořák, Z., Král, D., Thomas, R.: Testing first-order properties for subclasses of sparse graphs. J. ACM (JACM) 60(5), 36 (2013)
Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Perspectives in Mathematical Logic, 2nd edn. Springer, Heidelberg (1999)
Ebbinghaus, H.D., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Springer, Heidelberg (1994)
Frick, M., Grohe, M.: Deciding first-order properties of locally tree-decomposable structures. J. ACM 48, 1148–1206 (2001)
Gajarský, J., Hliněný, P., Lokshtanov, D., Obdržálek, J., Ordyniak, S., Ramanujan, M., Saurabh, S.: FO model checking on posets of bounded width. In: 2015 IEEE 56th Annual Symposium on Foundations of Computer Science (FOCS), pp. 963–974. IEEE (2015)
Gajarský, J., Hliněný, P., Obdržálek, J., Lokshtanov, D., Ramanujan, M.S.: A new perspective on FO model checking of dense graph classes. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 176–184. ACM (2016)
Ganian, R., Hliněný, P., Král’, D., Obdržálek, J., Schwartz, J., Teska, J.: FO model checking of interval graphs. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013. LNCS, vol. 7966, pp. 250–262. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39212-2_24
Geller, D.P.: The square root of a digraph. J. Combin. Theory 5, 320–321 (1968)
Grohe, M., Kreutzer, S., Siebertz, S.: Deciding first-order properties of nowhere dense graphs. In: Proceedings of the 46th Annual ACM Symposium on Theory of Computing, STOC 2014, pp. 89–98. ACM (2014)
Lampis, M.: Algorithmic meta-theorems for restrictions of treewidth. Algorithmica 64(1), 19–37 (2012)
Libkin, L.: Elements of Finite Model Theory. Texts in Theoretical Computer Science. Spinger, Heidelberg (2004)
Lin, Y.-L., Skiena, S.S.: Algorithms for square roots of graphs. In: Hsu, W.-L., Lee, R.C.T. (eds.) ISA 1991. LNCS, vol. 557, pp. 12–21. Springer, Heidelberg (1991). doi:10.1007/3-540-54945-5_44
Makowsky, J.: Algorithmic uses of the Feferman-Vaught theorem. Annals Pure Appl. Log. 126(1–3), 159–213 (2004)
Mnich, M., Rutter, I., Schmidt, J.M.: Linear-time recognition of map graphs with outerplanar witness. In: LIPIcs-Leibniz International Proceedings in Informatics, vol. 53. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)
Mukhopadhyay, A.: The square root of a graph. J. Comb. Theory 2, 290–295 (1967)
Nešetřil, J., de Mendez, P.O.: Sparsity – Graphs, Structures, and Algorithms. Algorithms and Combinatorics, vol. 28. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27875-4
Thorup, M.: Map graphs in polynomial time. In: Proceedings of 39th Annual Symposium on Foundations of Computer Science, pp. 396–405. IEEE (1998)
Tsukiyama, S., Ide, M., Ariyoshi, H., Shirakawa, I.: A new algorithm for generating all the maximal independent sets. SIAM J. Comput. 6(3), 505–517 (1977)
Tutte, W.T.: Graph Theory. Encyclopedia of Mathematics and its Applications, vol. 21. Cambridge University Press, Cambridge (2001)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer-Verlag GmbH Germany
About this paper
Cite this paper
Eickmeyer, K., Kawarabayashi, Ki. (2017). FO Model Checking on Map Graphs. In: Klasing, R., Zeitoun, M. (eds) Fundamentals of Computation Theory. FCT 2017. Lecture Notes in Computer Science(), vol 10472. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55751-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-662-55751-8_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-55750-1
Online ISBN: 978-3-662-55751-8
eBook Packages: Computer ScienceComputer Science (R0)