Graded modal logic and counting message passing automata
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911765159215104 |
|---|---|
| author | Ahvonen, Veeti Heiman, Damian Kuusisto, Antti |
| author_facet | Ahvonen, Veeti Heiman, Damian Kuusisto, Antti |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_06519 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Graded modal logic and counting message passing automata Ahvonen, Veeti Heiman, Damian Kuusisto, Antti Logic in Computer Science Distributed, Parallel, and Cluster Computing F.4.1; F.1.1; C.2.0 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. |
| title | Graded modal logic and counting message passing automata |
| topic | Logic in Computer Science Distributed, Parallel, and Cluster Computing F.4.1; F.1.1; C.2.0 |
| url | https://arxiv.org/abs/2401.06519 |