|Abstract of Paper|
Constructing Infinite Graphs With
by Wolfgang Thomas
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 $\mu$-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.