[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Efficient First-Order Model-Checking Using Short Labels

  • Conference paper
Frontiers in Algorithmics (FAW 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5059))

Included in the following conference series:

  • 1438 Accesses

Abstract

We prove that there exists an O(log(n))-labeling scheme for every first-order formula with free set variables in every class of graphs that is nicely locally cwd-decomposable, which contains in particular, the nicely locally tree-decomposable classes. For every class of graphs of bounded expansion we prove that every bounded formula has an O(log(n))-labeling scheme. We also prove that every quantifier-free formula has an O(log(n))-labeling scheme in graphs of bounded arboricity. Some of these results are extended to counting queries.

Research supported by the project “Graph decompositions and Algorithms (GRAAL)” of “Agence Nationale pour la Recherche”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Bodlaender, H.L.: A Linear-Time Algorithm for Finding Tree-Decompositions of Small Tree-width. SIAM J. Comput. 25(6), 1305–1317 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  2. Courcelle, B., Gavoille, C., Kanté, M.M., Twigg, A.: Optimal Labeling for Connectivity Checking in Planar Networks with Obstacles. (manuscript, 2008); An extended abstract will appear in Electronic Notes in Discrete Mathematics. In: Proceedings of the first Conference Topological and Geometric Graph Theory, Paris (2008)

    Google Scholar 

  3. Courcelle, B., Olariu, S.: Upper Bounds to the Clique-Width of Graphs. Discrete Applied Mathematics 101(1-3), 77–114 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  4. Courcelle, B., Twigg, A.: Compact Forbidden-Set Routing. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 37–48. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Courcelle, B., Vanicat, R.: Query Efficient Implementation of Graphs of Bounded Clique-Width. Discrete Applied Mathematics 131(1), 129–150 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  6. Dawar, A., Grohe, M., Kreutzer, S.: Locally Excluding a Minor. In: 22nd IEEE Symposium on Logic in Computer Science (LICS), pp. 270–279. IEEE Computer Society, Los Alamitos (2007)

    Google Scholar 

  7. Durand, A., Grandjean, E.: First-Order Queries on Structures of Bounded Degree are Computable with Constant Delay. ACM Trans. Comput. Log 8(4) (2007)

    Google Scholar 

  8. Frick, M.: Generalized Model-Checking over Locally Tree-Decomposable Classes. Theory Comput. Syst. 37(1), 157–191 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  9. Frick, M., Grohe, M.: Deciding First-Order Properties of Locally Tree-Decomposable Structures. J. ACM 48(1), 1184–1206 (2001)

    Article  MathSciNet  Google Scholar 

  10. Gaifman, H.: On Local and Non-Local Properties. In: Proceedings of the Herbrand Symposium Logic Colloquium 1981, pp. 105–135 (1982)

    Google Scholar 

  11. Grohe, M.: Logic, Graphs and Algorithms. In: Flum, Grädel, Wilke (eds.) Logic, Automata, History and Perspectives, pp. 357–422. Amsterdam University Press (2007)

    Google Scholar 

  12. Gavoille, C., Peleg, D.: Compact and Localized Distributed Data Structures. Distributed Computing 16(2-3), 111–120 (2003)

    Article  Google Scholar 

  13. Hliněný, P., Oum, S.: Finding Branch-Decompositions and Rank-Decompositions. In: Arge, L., Hoffmann, M., Welzl, E. (eds.) ESA 2007. LNCS, vol. 4698, pp. 163–174. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Lozin, V.: Clique-Width of Unit Interval Graphs. arXiv:0709.1935 (manuscript, 2007)

    Google Scholar 

  15. Nešetřil, J., Ossona de Mendez, P.: Linear Time Low Tree-Width Partitions and Algorithmic Consequences. In: Kleinberg, J.M. (ed.) 38th Annual ACM Symposium on Theory of Computing (STOC), pp. 391–400. ACM, New York (2006)

    Google Scholar 

  16. Robertson, N., Seymour, P.: Graph Minors V: Excluding a Planar Graph. J. Combin. Theory Ser. B 41(1), 92–114 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  17. Seese, D.: Linear Time Computable Problems and First-Order Descriptions. Mathematical Structures in Computer Science 6(6), 505–526 (1996)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LaBRI, CNRS, Université de Bordeaux, France

    Bruno Courcelle, Cyril Gavoille & Mamadou Moustapha Kanté

Authors
  1. Bruno Courcelle
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cyril Gavoille
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mamadou Moustapha Kanté
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Franco P. Preparata Xiaodong Wu Jianping Yin

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Courcelle, B., Gavoille, C., Kanté, M.M. (2008). Efficient First-Order Model-Checking Using Short Labels. In: Preparata, F.P., Wu, X., Yin, J. (eds) Frontiers in Algorithmics. FAW 2008. Lecture Notes in Computer Science, vol 5059. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69311-6_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-69311-6_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69310-9

  • Online ISBN: 978-3-540-69311-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation