Tags:expressiveness, model theory and separated relations

Abstract:

We compare the model-theoretic expressiveness of the symbolic heap fragment of Separation Logic (SL) with inductive definitions with (Monadic) Second Order Logic ((M)SO). While SL and MSO are incomparable on structures of unbounded treewidth, it turns out that SL can be embedded in SO and that MSO becomes a strict subset of SL, when the treewidth of the models is bounded by a constant and the relation symbols have arity one or two. We leave open the problems of equivalence between (M)SO and SL on bounded treewidth models over signatures containing relation symbols of arity three or more.

On the Expressiveness of a Logic of Separated Relations