Graph neural networks and MSO

Key Points

• The proof demonstrates that graph neural networks can capture all MSO-definable node properties over trees, enhancing understanding of their capabilities.
• Using distributed automata in the proof effectively shows the equivalence to graded modal substitution calculus, providing a different perspective on expressive power.
• Variants of acceptance conditions were considered to further explore the implications and nuances of this equivalence in graph neural networks.
• This work supports advancing the theoretical foundations of graph neural networks and their applications in logic-based frameworks.