Effective MSO-Definability for Tree-width Bounded Models of an Inductive Separation Logic of Relations

Lucas Bueri, Radu Iosif, Florian Zuleger

A class of graph languages is definable in Monadic Second-Order logic (MSO) if and only if it consists of sets of models of MSO formulæ. If, moreover, there is a computable bound o…