2024/01/12 by Ahvonen, Veeti, Heiman, Damian, Kuusisto, Antti
#C.2.0 #Distributed #F.1.1 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Parallel #and Cluster Computing (cs.DC)
paper · doi:10.48550/arxiv.2401.06519
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.