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.

翻译：研究了分级(多)模态逻辑与计数(多通道)消息传递自动机之间的关系，并探讨了其在Weisfeiler-Leman算法中的应用。我们引入了分级模态类型的概念，即编码带指点Kripke模型局部信息的分级模态逻辑公式。同时提出了执行Weisfeiler-Leman算法在图节点区分中推广形式的消息传递自动机。研究表明，这些自动机可识别的带指点Kripke模型类可由可数(可能无穷)个分级模态公式的析取定义，反之亦然。特别地，该等价性在递归可枚举析取与递归可枚举自动机之间同样成立。我们还展示了利用一阶逻辑(已扩充Härtig量词与最大不动点)公式实现Weisfeiler-Leman算法的方法。