Abstract of Paper

Constructing Infinite Graphs With Decidable MSO-Theory
by Wolfgang Thomas

Abstract:

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.