Graph logic (GL) is a spatial logic for querying graphs introduced by Cardelli et al. It has been observed that in terms of expressive power, this logic is a fragment of Monadic Second Order Logic (MSO), with quantification over sets of edges. We show that the containment is proper by exhibiting a property that is not GL definable but is definable in MSO, even in the absence of quantification over labels. Moreover, this holds when the graphs are restricted to be forests and thus strengthens in several ways a result of Marcinkowski. As a consequence we also obtain that Separation Logic, with a separating conjunction but without the magic wand, is strictly weaker than MSO over memory heaps, settling an open question of Brochenin et al. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Antonopoulos, T., & Dawar, A. (2009). Separating graph logic from mso. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5504 LNCS, pp. 63–77). https://doi.org/10.1007/978-3-642-00596-1_6
Mendeley helps you to discover research relevant for your work.