Graded modal logic and counting message passing automata

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.