Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Graded modal logic and counting message passing automata

Veeti Ahvonen, Damian Heiman, Antti Kuusisto

TL;DR

The paper addresses how graded multimodal logic relates to counting multichannel message passing automata and the Weisfeiler-Leman algorithm. It develops GMML, GMML-types, and CMMPA, showing a precise equivalence: pointed Kripke-model classes recognizable by CMMPA correspond exactly to classes definable by countable disjunctions of GMML formulas, with the equivalence extending to recursively enumerable cases and connecting WL to GMML via type automata. It also presents an FO-based characterization of WL using Härtig's quantifier and greatest fixed points, providing a unified view of logical and automata-theoretic perspectives on graph isomorphism testing and potential neural-network interpretations. The results bridge descriptive complexity, distributed computation, and graph-algorithm relaxation, and point to future work on infinite models and deeper logical encodings of WL-like processes.

Abstract

We examine the relationship of graded (multi)modal logic to counting (multichannel) message passing automata with applications to the Weisfeiler-Leman algorithm. We introduce the notion of graded multimodal types, which are formulae of graded multimodal logic that encode the local information of a pointed Kripke-model. We also introduce message passing automata that carry out a generalization of the Weisfeiler-Leman algorithm for distinguishing non-isomorphic graph nodes. We show that the classes of pointed Kripke-models recognizable by these automata are definable by a countable (possibly infinite) disjunction of graded multimodal formulae and vice versa. In particular, this equivalence also holds between recursively enumerable disjunctions and recursively enumerable automata. We also show a way of carrying out the Weisfeiler-Leman algorithm with a formula of first order logic that has been augmented with Härtig's quantifier and greatest fixed points.

Graded modal logic and counting message passing automata

TL;DR

The paper addresses how graded multimodal logic relates to counting multichannel message passing automata and the Weisfeiler-Leman algorithm. It develops GMML, GMML-types, and CMMPA, showing a precise equivalence: pointed Kripke-model classes recognizable by CMMPA correspond exactly to classes definable by countable disjunctions of GMML formulas, with the equivalence extending to recursively enumerable cases and connecting WL to GMML via type automata. It also presents an FO-based characterization of WL using Härtig's quantifier and greatest fixed points, providing a unified view of logical and automata-theoretic perspectives on graph isomorphism testing and potential neural-network interpretations. The results bridge descriptive complexity, distributed computation, and graph-algorithm relaxation, and point to future work on infinite models and deeper logical encodings of WL-like processes.

Abstract

We examine the relationship of graded (multi)modal logic to counting (multichannel) message passing automata with applications to the Weisfeiler-Leman algorithm. We introduce the notion of graded multimodal types, which are formulae of graded multimodal logic that encode the local information of a pointed Kripke-model. We also introduce message passing automata that carry out a generalization of the Weisfeiler-Leman algorithm for distinguishing non-isomorphic graph nodes. We show that the classes of pointed Kripke-models recognizable by these automata are definable by a countable (possibly infinite) disjunction of graded multimodal formulae and vice versa. In particular, this equivalence also holds between recursively enumerable disjunctions and recursively enumerable automata. We also show a way of carrying out the Weisfeiler-Leman algorithm with a formula of first order logic that has been augmented with Härtig's quantifier and greatest fixed points.
Paper Structure (9 sections, 9 theorems, 14 equations)

This paper contains 9 sections, 9 theorems, 14 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Graded multimodal logic
  4. Graded multimodal types
  5. Message passing automata
  6. The Weisfeiler-Leman algorithm and type automata
  7. GMML-formulae capture CMMPA-recognizable classes
  8. Expressing WL via first-order logic with Härtig's quantifier and greatest fixed points
  9. Conclusion

Key Result

Proposition 2.1

Let $\Pi$ be a finite set of proposition symbols and $I = [a]$ a set of indices (where $a \in \mathbb Z_+$). Given two countable (possibly infinite) disjunctions of $(\Pi, I)$-formulae of $\mathrm{GMML}$$\bigvee_{\varphi \in S} \varphi$ and $\bigvee_{\psi \in S'} \psi$, we have that $\bigvee_{\varph

Theorems & Definitions (16)

  • Proposition 2.1
  • proof
  • Remark 2.2
  • Lemma 3.1
  • proof
  • Theorem 3.2
  • proof
  • Lemma 3.3
  • proof
  • Theorem 3.4
  • ...and 6 more