The monadic second-order logic of graphs. I: Recognizable sets of finite graphs. (English) Zbl 0722.03008

Courcelle, Bruno

Inf. Comput. 85, No. 1, 12-75 (1990).

The paper begins an investigation of the monadic second-order logic of graphs and of sets of graphs, using techniques from universal algebra and the theory of formal languages. The author introduces a recognizable set in a many-sorted algebra, defines graphs and the operations on graphs, and obtains a many-sorted algebra of graphs. Considering graphs as logical structures, the author introduces the counting monadic second- order logic and the associated definable sets of graphs. The main result of the paper says that every definable set of graphs is recognizable. It follows that, for every graph property expressible in counting monadic second-order logic, the set of graphs satisfying this property, and belonging to a given context-free set of graphs forms a context-free set. The author proves that the monadic second-order theory of a context-free set of graphs is decidable. Finally, the author deals with unordered unbounded trees, proves that a set of finite unordered unbounded trees is recognizable iff it is definable in counting monadic second-order logic, and the counting monadic second-order logic is strictly more powerful than the “ordinary” one, in arbitrary logical structures.

Reviewer: Li Xiang (Guiyang)

MSC:

03B15	Higher-order logic; type theory (MSC2010)
68R10	Graph theory (including graph drawing) in computer science
05C75	Structural characterization of families of graphs
05C65	Hypergraphs
03B25	Decidability of theories and sets of sentences
68Q45	Formal languages and automata
08A70	Applications of universal algebra in computer science

Keywords:

definability; recognition; decidability; monadic second-order logic of graphs; universal algebra; formal languages; many-sorted algebra of graphs; context-free set

References:

[1]	Arnborg, S.; Lagergren, J.; Seese, D., Problems easy for tree decomposable graphs, (), 38-51
[2]	Bauderon, M.; Courcelle, B., Graph expressions and graph rewritings, Math. systems theory, 20, 83-127, (1987) · Zbl 0641.68115
[3]	Bodlaender, H., Dynamic programming on graphs with bounded tree width, (), 105-118
[4]	Büchi, J., Weak 2nd order logic and finite automata, Z. math. logik gründlag. math., 5, 66-92, (1960) · Zbl 0103.24705
[5]	Courcelle, B., Equivalences and transformations of regular systems. applications to recursive program schemes and grammars, Theoret. comput. sci., 42, 1-122, (1986) · Zbl 0636.68104
[6]	Courcelle, B., An axiomatic definition of context-free rewriting and its application to NLC graph grammars, Theoret. comput. sci., 55, 141-181, (1987) · Zbl 0644.68095
[7]	Courcelle, B., A representation of graph by algebraic expressions and its use for graph rewriting systems, (), 112-132
[8]	Courcelle, B., On context-free sets of graphs and their monadic second order theory, (), 133-146
[9]	Courcelle, B., On using context-free graph grammars for analyzing recursive definitions, (), 83-122
[10]	Courcelle, B., On recognizable sets and tree automata, ()
[11]	{\scCourcelle, B.} (in press), Graph rewriting: an algebraic and logical approach, in “Handbook of Theoretical Computer Science” (J. Van Leeuwen, Ed.), Elsevier, Amsterdam.
[12]	Courcelle, B., The monadic second-order logic of graphs: definable sets of finite graphs, (), 30-53
[13]	Courcelle, B., The monadic second-order logic of graphs. II. infinite graphs of bounded width, Math. systems theory, 21, 187-221, (1989) · Zbl 0694.68043
[14]	Courcelle, B., (), submitted for publication
[15]	Courcelle, B., The monadic second-order logic of graphs. IV. every equational graph Is definable, (1988), Research Report 8830, submitted for publication
[16]	Doner, J., Tree acceptors and some of their applications, J. comput. system sci., 4, 406-451, (1970) · Zbl 0212.02901
[17]	Ehrig, H.; Mahr, B., ()
[18]	Eilenberg, S.; Wright, J., Automata in general algebras, Inform. and control, 11, 52-70, (1967) · Zbl 0175.27902
[19]	Gaifmann, H., Local and non-local properties, (), 105-135
[20]	Gecseg, F.; Steinby, M., ()
[21]	Habel, A.; Kreowski, H.J., May we introduce to you, hyperedge replacement, (), 15-26 · Zbl 0643.68106
[22]	Johnson, D., The NP-completeness column: an on-going guide (16th), J. algorithms, 6, 434-451, (1985) · Zbl 0608.68032
[23]	Lautemann, C., Efficient algorithms on context-free graph grammars, (), 362-378
[24]	Lengauer, T.; Wanke, E., Efficient analysis of graph properties on context-free graph languages, (), 379-393
[25]	Mezei, J.; Wright, J., Algebraic automata and context-free sets, Inform. and control, 11, 3-29, (1967) · Zbl 0155.34301
[26]	Rozenberg, G.; Salomaa, A., ()
[27]	Seese, D., Ein unentscheidbarkeitskriterium, Wiss. Z. humbold-univ. Berlin math.-natur. Reich, 24, 772-780, (1975) · Zbl 0331.02026
[28]	{\scSeese, D.} (in press), The structure of the models of decidable monadic theories of graphs, Annals of Pure Appl. Logic.
[29]	{\scThomas, W.} (in press), Automata on infinite objects, in “Handbook of Theoretical Computer Science” (J. Van Leeuwen, Ed.), Elsevier, Amsterdam.
[30]	Trahtenbrot, B., Impossibility of an algorithm for the decision problem on finite classes, Dokl. nauk. SSSR, 70, 569-572, (1950) · Zbl 0038.15001
[31]	{\scWirsing, M.} (in press), Algebraic specification, in “Handbook of Theoretical Computer Science” (J. Van Leeuwen, Ed.), Elsevier, Amsterdam.