This introductory paper reports on recent progress in the search for classes of infinite graphs where interesting model-checking problems are decidable. We consider properties expressible in monadic second-order logic (MSO-logic), a formalism which encompasses standard temporal logics and the modal μ-calculus. We discuss a class of infinite graphs proposed by D. Caucal (in MFCS 2002) which can be generated from the infinite binary tree by applying the two processes of MSO-interpretation and of unfolding. The main purpose of the paper is to give a feeling for the rich landscape of infinite structures in this class and to point to some questions which deserve further study. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Thomas, W. (2003). Constructing infinite graphs with a decidable MSO-theory. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2747, 113–124. https://doi.org/10.1007/978-3-540-45138-9_6
Mendeley helps you to discover research relevant for your work.