×

zbMATH — the first resource for mathematics

On the model-checking of monadic second-order formulas with edge set quantifications. (English) Zbl 1236.05143
Summary: We extend clique-width to graphs with multiple edges. We obtain fixed-parameter tractable model-checking algorithms for certain monadic second-order graph properties that depend on the multiplicities of edges, with respect to this “new” clique-width. We define special tree-width, the variant of tree-width relative to tree-decompositions such that the boxes that contain a vertex are on a path originating from some fixed node. We study its main properties. This definition is motivated by the construction of finite automata associated with monadic second-order formulas using edge set quantifications. These automata yield fixed-parameter linear algorithms with respect to tree-width for the model-checking of these formulas. Their construction is much simpler for special tree-width than for tree-width, for reasons that we explain.

MSC:
05C69 Vertex subsets with special properties (dominating sets, independent sets, cliques, etc.)
03B15 Higher-order logic; type theory (MSC2010)
05C70 Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.)
05C12 Distance in graphs
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bodlaender, H.; Engelfriet, J., Domino tree-width, J. algorithms, 24, 94-123, (1997) · Zbl 0882.68106
[2] Cameron, K.; Hoàng, C.; Lévêque, B., Asteroids in rooted and directed path graphs, Electron. notes discrete math., 32, 67-74, (2009) · Zbl 1267.05174
[3] H. Comon, et al., Tree automata techniques and applications, On line for free at: http://tata.gforge.inria.fr/.
[4] Corneil, D.; Rotics, U., On the relationship between clique-width and treewidth, SIAM J. comput., 34, 825-847, (2005) · Zbl 1069.05067
[5] Courcelle, B., The monadic second-order logic of graphs I: recognizable sets of finite graphs, Inform. and comput., 85, 12-75, (1990) · Zbl 0722.03008
[6] B. Courcelle, Graph Structure and Monadic Second-Order Logic, Book to be Published by Cambridge University Press. Readable on: http://www.labri.fr/perso/courcell/Book/CourGGBook.pdf.
[7] B. Courcelle, I. Durand, Verifying monadic second-order graph properties with tree automata, in: C. Rhodes (Ed.), 3rd European Lisp Symposium, Lisbon, Informal Proceedings, May 2010, pp. 7-21. See: http://www.labri.fr/perso/courcell/ArticlesEnCours/BCDurandLISP.pdf.
[8] B. Courcelle, I. Durand, Automata for the verification of monadic second-order graph properties (2011) (in preparation). · Zbl 1285.03049
[9] 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) · Zbl 1009.68102
[10] Courcelle, B.; Olariu, S., Upper bounds to the clique-width of graphs, Discrete appl. math., 101, 77-114, (2000) · Zbl 0958.05105
[11] Diestel, R., Graph theory, (2005), Springer · Zbl 1074.05001
[12] Downey, R.; Fellows, M., Parameterized complexity, (1999), Springer · Zbl 0961.68533
[13] Fellows, M.; Rosamond, F.; Rotics, U.; Szeider, S., Clique-width is NP-complete, SIAM J. discrete math., 23, 909-939, (2009) · Zbl 1207.68159
[14] Flum, J.; Grohe, M., Parametrized complexity theory, (2006), Springer · Zbl 1143.68016
[15] Frick, M.; Grohe, M., The complexity of first-order and monadic second-order logic revisited, Ann. pure appl. logic, 130, 3-31, (2004) · Zbl 1062.03032
[16] Gavril, F., A recognition algorithm for the intersection graphs of directed paths in directed trees, Discrete math., 13, 237-249, (1975) · Zbl 0312.05108
[17] Golumbic, M.; Rotics, U., On the clique-width of certain perfect graph classes, Internat. J. found. comput. sci., 11, 423-443, (2000) · Zbl 1320.05090
[18] Hliněný, P.; Oum, S., Finding branch-decompositions and rank-decompositions, SIAM J. comput., 38, 1012-1032, (2008) · Zbl 1163.05331
[19] Libkin, L., Elements of finite model theory, (2004), Springer · Zbl 1060.03002
[20] Oum, S.; Seymour, P., Approximating clique-width and branch-width, J. combin. theory ser. B, 96, 514-528, (2006) · Zbl 1114.05022
[21] Seese, D., Tree-partite graphs and the complexity of algorithms (extended abstract), (), 412-421
[22] Stockmeyer, L.; Meyer, A., Cosmological lower bound on the circuit complexity of a small problem in logic, J. ACM, 49, 753-784, (2002) · Zbl 1326.68153
[23] Weyer, M., Decidability of S1S and S2S, (), 207-230 · Zbl 1021.03001
[24] Wood, D., On tree-partition-width, European J. combin., 30, 1245-1253, (2009) · Zbl 1205.05079
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.