Thiagarajan's MSO decidability conjecture for grid-free trace-regular event structures

Let ${\mathcal E}_N$ be a trace-regular event structure, and let $\operatorname{MSO}({\mathcal E}_N)$ denote its monadic second-order theory. The event structure is grid-free when it contains no three pairwise disjoint infinite event sets satisfying the grid conditions described in the paper. Thiagarajan's MSO decidability conjecture. The $\operatorname{MSO}$ theory of a trace-regular event structure ${\mathcal E}_N$ is decidable if and only if ${\mathcal E}_N$ is grid-free. The paper presents this as an open conjecture; it also records that non-grid-free systems have undecidable MSO theory.