Formula size game and model checking for modal substitution calculus

TL;DR

This paper develops a twofold methodological framework for MSC and its variants: a formula-size game that captures expressivity across MSC, GMSC, GGMSC, and SC, and a thorough model-checking analysis that ties these logics to linear tape-bounded Turing machines and modal μ-calculus variants. It shows that MSC and its extensions are as expressive as linear tape-bounded TMs, while asynchronous variants align with MCL and the μ-fragment of the global graded μ-calculus, and establishes PSPACE-completeness for combined/data model checking (PTIME for asynchronous variants). Additionally, it proves a PSPACE/NP dichotomy for SC’s satisfiability and model checking, and provides a universal, computable reduction from recursively enumerable problems to MSC model checking, highlighting the theoretical limits of these logics. Collectively, the results illuminate deep connections between descriptive complexity, formal game semantics, and canonical computation models, with implications for reasoning about neural networks, distributed systems, and logic-based verification.

Abstract

Recent research has applied modal substitution calculus (MSC) and its variants to characterize various computational frameworks such as graph neural networks (GNNs) and distributed computing systems. For example, it has been shown that the expressive power of recurrent graph neural networks coincides with graded modal substitution calculus GMSC, which is the extension of MSC with counting modalities. GMSC can be further extended with the counting global modality, resulting in the logic GGMSC which corresponds to GNNs with global readout mechanisms. In this paper we introduce a formula-size game that characterizes the expressive power of MSC, GMSC, GGMSC, and related logics. Furthermore, we study the expressiveness and model checking of logics in this family. We prove that MSC and its extensions (GMSC, GGMSC) are as expressive as linear tape-bounded Turing machines, while asynchronous variants are linked to modal mu-calculus and modal computation logic MCL. We establish that for MSC, GMSC and GGMSC, both combined and data complexity of model checking are PSPACE-complete, and for their asynchronous variants, both complexities are PTIME-complete. We also establish that for the propositional fragment SC of MSC, the combined complexity of model checking is PSPACE-complete, while for asynchronous SC it is PTIME-complete, and in both cases, data complexity is constant. As a corollary, we observe that SC satisfiability is PSPACE-complete and NP-complete for its asynchronous variant. Finally, we construct a universal reduction from all recursively enumerable problems to MSC model checking.

Figures (1)

• Figure 1: Below, on the left we have a program $\Lambda$ with two base rules (in red) and two induction rules (in blue) and on the right we have its syntax forest $\mathcal{F}_\Lambda$. The two blue trees correspond to the bodies of the induction rules while the red ones correspond to the bodies of the base rules. Back edges are drawn as dotted edges. The size of the program and its syntax forest is $19$. If $v$ is the node labeled by $\Diamond_{\geq 2}$ in $\mathcal{F}_\Lambda$, then $\Lambda_v = \Diamond_{\geq 2} X$.

Theorems & Definitions (42)

• Example 2.1
• Lemma 2.2
• proof
• Remark 3.1
• Theorem 3.2
• proof
• Remark 3.3
• Theorem 3.4
• proof
• Remark 3.5