Graded modal logic and counting message passing automata
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\"artig's quantifier and greatest fixed points.
Keywords
Cite
@article{arxiv.2401.06519,
title = {Graded modal logic and counting message passing automata},
author = {Veeti Ahvonen and Damian Heiman and Antti Kuusisto},
journal= {arXiv preprint arXiv:2401.06519},
year = {2024}
}