The monadic second-order logic of graphs. II: Infinite graphs of bounded width. (English) Zbl 0694.68043

Courcelle, Bruno

Math. Syst. Theory 21, No. 4, 187-221 (1989).

From the author’s introduction: “Finite graphs can be denoted by algebraic expressions M. Bauderon and B. Courcelle [Math. Syst. Theory 20, No.2/3, 83-127 (1987; Zbl 0641.68115)] that are constructed over an infinite signature \({\mathbb{H}}\). Infinite graph expressions can be defined, and they denote countable graphs. With finitely many operators, we cannot denote all countable graphs, but only those of finite width. These infinite graph expressions are actually infinite trees. On the other hand, Courcelle has defined... a monadic second order logical language appropriate for expressing properties of graphs. Our main theorem states that given a finite subset \({\mathbb{K}}\) of \({\mathbb{H}}\), and a monadic second-order formula \(\phi\), we can construct a monadic second-order formula that defines the set \({\mathbb{E}}({\mathbb{K}},\phi)\) of finite or infinite graph expressions constructed over \({\mathbb{K}}\), the corresponding graph of which satisfies \(\phi\). From Rabin’s theorem, saying that the monadic second-order theory of the complete binary tree is decidable, it follows that the emptiness of the set \({\mathbb{E}}({\mathbb{K}},\phi)\) is decidable. Hence the monadic second-order theory of all countable graphs, of width less than some fixed integer is decidable.” The paper is carefully and clearly written, with enough examples to make reading relatively easy.

Reviewer: S.Bloom

MSC:

68R10	Graph theory (including graph drawing) in computer science
03B15	Higher-order logic; type theory (MSC2010)
05C99	Graph theory
68Q60	Specification and verification (program logics, model checking, etc.)

Keywords:

second-order logic of graphs; decidability

Citations:

Zbl 0641.68115

References:

[1]	Bauderon, M., On systems of equations defining infinite graphs,Proceedings of the Colloquium on Graph Theoretic Concepts in Computer Science (WG’88), June 1988, Amsterdam, Springer-Verlag, Berlin, to appear.
[2]	Bauderon, M., Infinite hypergraphs, in preparation. · Zbl 0758.05069
[3]	Bauderon, M., and Courcelle, B., Graph expressions and graph rewritings,Math. Systems Theory,20 (1987), 83–127. · Zbl 0641.68115
[4]	Courcelle, B., Fundamental properties of infinite trees,Theoret. Comput. Sci.,25 (1983), 95–169. · Zbl 0521.68013
[5]	Courcelle, B., Equivalences and transformations of regular systems.Applications to recursive program schemes, Theoret. Comput. Sci.,42 (1986), 1–122. · Zbl 0636.68104
[6]	Courcelle, B., An axiomatic definition of context-free rewriting, and its application to NLC graph grammars,Theoret. Comput. Sci.,55 (1987), 141–181. · Zbl 0644.68095
[7]	Courcelle, B., A representation of graphs by algebraic expressions and its use for graph rewriting systems,Proceedings of the Third Internal Workshop on Graph Grammars, Lecture Notes in Computer Science, Vol. 291, Springer-Verlag, Berlin, 1987, pp. 112–132. · Zbl 0643.68104
[8]	Courcelle, B., On context-free sets of graphs and their monadic 2nd-order theory,Proceedings of the Third Internal Workshop on Graph Grammars, Lecture Notes in Computer Science, Vol. 291, Springer-Verlag, Berlin, 1987, pp. 133–146. · Zbl 0643.68105
[9]	Courcelle, B., On using context-free graph grammars for analyzing recursive definitions, inProgramming of Future Generation Computers, II (K. Fuchi, L. Kott, eds.), Elsevier, Amsterdam, 1988, pp. 83–122.
[10]	Courcelle, B., The monadic second-order logic of graphs, I: Recognizable sets of finite graphs, Report I-8837, submitted. · Zbl 0722.03008
[11]	Courcelle, B., The monadic second-order logic of graphs, III: Tree-width, forbidden minors and complexity issues, Report I-8852, submitted. · Zbl 0754.03006
[12]	Courcelle, B., The monadic second-order logic of graphs, IV: Every equational graph is definable, Report I-8830, submitted. · Zbl 0731.03006
[13]	Courcelle, B., Recursive applicative program schemes, inHandbook of Theoretical Computer Science, J. Van Leeuwen, ed., Elsevier, Amsterdam, to appear.
[14]	Doner, J., Tree acceptors and some of their applications,J. Comput. System Sci.,4 (1970), 406–451. · Zbl 0212.02901
[15]	Goguen, J., Thatcher, J., and Wagner, E., An initial algebra approach to the specification, correctness and implementation of abstract data types, inCurrent Trends in Programming Methodology, R. Yeh, ed., Prentice-Hall, Englewood Cliffs, NJ, 1978, pp. 80–149.
[16]	Goguen, J., Thatcher, J., Wagner, E., and Wright, J., Initial algebra semantics and continuous algebras,Assoc. Comput. Mach.,24 (1977), 68–95. · Zbl 0359.68018
[17]	Guessarian, I.,Algebraic Semantics, Lecture Notes in Computer Science, Vol. 99, Springer-Verlag, Berlin, 1981. · Zbl 0474.68010
[18]	Gurevich, Y., Toward logic tailored for computational complexity, inComputation and Proof Theory, M. Richter, ed., Lecture Notes in Mathematics, Vol. 1104, Springer-Verlag, Berlin, 1984, pp. 175–216.
[19]	Muller, D, and Schupp, P., The theory of ends, pushdown automata and second-order logic,Theoret. Comput. Sci.,37 (1985), 51–75. · Zbl 0605.03005
[20]	Nivat, M., Genealogies, unpublished report, University of Paris 7, 1987.
[21]	Rabin, M., Decidability of 2nd-order theories and automata on infinite trees,Trans. Amer. Math. Soc.,141 (1969), 1–35. · Zbl 0221.02031
[22]	Rabin, M.,Automata on Infinite objects and Church’s Problem, Regional Conference Series in Mathematics, Vol. 13, A.M.S., Providence, RI, 1972. · Zbl 0315.02037
[23]	Seese, D., The structure of the models of decidable monadic theories,J. Pure Appl. Logic, to appear. · Zbl 0733.03026
[24]	Seese, D., Ordered tree-representations of infinite graphs, Preprint, Akademie der DDR, Berlin, East Germany, 1987.
[25]	Trahtenbrot, B., Impossibility of an algorithm for the decision problem on finite classes,Dokl. Akad. Nauk. SSSR,70 (1950), 569–572.