On modal characterisation theorems over finite structures with applications to graph neural networks
Bisimulations capture a natural notion of equivalence for elements in relational structures, which was independently discovered in different areas of computer science. The relevance of bisimulations across fields naturally motivates the characterisation of the bisimulation-invariant fragments for va...
| Huvudupphovsman: | |
|---|---|
| Övriga upphovsmän: | |
| Materialtyp: | Lärdomsprov |
| Språk: | English |
| Publicerad: |
2024
|
| _version_ | 1826315202750054400 |
|---|---|
| author | Pflüger, MF |
| author2 | Kostylev, E |
| author_facet | Kostylev, E Pflüger, MF |
| author_sort | Pflüger, MF |
| collection | OXFORD |
| description | Bisimulations capture a natural notion of equivalence for elements in relational structures, which was independently discovered in different areas of computer science. The relevance of bisimulations across fields naturally motivates the characterisation of the bisimulation-invariant fragments for various logics. Famously, a seminal theorem by van Benthem characterises the bisimulation-invariant fragment of first-order logic (FOL) in terms of modal logic. Similarly, Janin and Walukiewicz showed that the bisimulation-invariant fragment of monadic second-order logic (MSO) corresponds precisely to the (modal) mu-calculus. Notably, neither van Benthem’s nor Janin and Walukiewicz’s argument immediately carries over when only considering finite structures. In the case of FOL, Rosen provided an alternative proof, which also holds in the relativised setting. However, further modal characterisations for stronger notions of bisimulation and any logic more expressive than FOL over finite structures have remained long-standing open problems in finite model theory. In this thesis, we answer several of these open problems. In particular, as our main result, we prove that, over finite structures, every two-way bisimulation-invariant parameter-free monadic least fixpoint logic formula, a well-known logic in between FOL and MSO, is equivalent to a formula in the two-way mu-calculus and vice versa. Moreover, in a second line of work, we show that multiple notions of bisimulations considered in this thesis capture natural notions of invariance in graph learning. In particular, we show that node classifiers, functions mapping graphs to subsets of their nodes, realised by several classes of Graph Neural Networks (GNNs) can, in each case, be characterised by invariance under a variant of bisimulations. Finally, given our semantic characterisations of the considered GNN classes in terms of invariance under bisimulations, we show that we can obtain conditional logical characterisations for the node classifiers realised by the considered GNN classes through applications of our modal characterisation theorems. |
| first_indexed | 2024-12-09T03:21:41Z |
| format | Thesis |
| id | oxford-uuid:18df85f7-1b7f-47fa-8ac5-08cfa0c9a438 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-12-09T03:21:41Z |
| publishDate | 2024 |
| record_format | dspace |
| spelling | oxford-uuid:18df85f7-1b7f-47fa-8ac5-08cfa0c9a4382024-11-15T14:13:32ZOn modal characterisation theorems over finite structures with applications to graph neural networksThesishttp://purl.org/coar/resource_type/c_db06uuid:18df85f7-1b7f-47fa-8ac5-08cfa0c9a438EnglishHyrax Deposit2024Pflüger, MFKostylev, EHorrocks, ICuenca Grau, BBisimulations capture a natural notion of equivalence for elements in relational structures, which was independently discovered in different areas of computer science. The relevance of bisimulations across fields naturally motivates the characterisation of the bisimulation-invariant fragments for various logics. Famously, a seminal theorem by van Benthem characterises the bisimulation-invariant fragment of first-order logic (FOL) in terms of modal logic. Similarly, Janin and Walukiewicz showed that the bisimulation-invariant fragment of monadic second-order logic (MSO) corresponds precisely to the (modal) mu-calculus. Notably, neither van Benthem’s nor Janin and Walukiewicz’s argument immediately carries over when only considering finite structures. In the case of FOL, Rosen provided an alternative proof, which also holds in the relativised setting. However, further modal characterisations for stronger notions of bisimulation and any logic more expressive than FOL over finite structures have remained long-standing open problems in finite model theory. In this thesis, we answer several of these open problems. In particular, as our main result, we prove that, over finite structures, every two-way bisimulation-invariant parameter-free monadic least fixpoint logic formula, a well-known logic in between FOL and MSO, is equivalent to a formula in the two-way mu-calculus and vice versa. Moreover, in a second line of work, we show that multiple notions of bisimulations considered in this thesis capture natural notions of invariance in graph learning. In particular, we show that node classifiers, functions mapping graphs to subsets of their nodes, realised by several classes of Graph Neural Networks (GNNs) can, in each case, be characterised by invariance under a variant of bisimulations. Finally, given our semantic characterisations of the considered GNN classes in terms of invariance under bisimulations, we show that we can obtain conditional logical characterisations for the node classifiers realised by the considered GNN classes through applications of our modal characterisation theorems. |
| spellingShingle | Pflüger, MF On modal characterisation theorems over finite structures with applications to graph neural networks |
| title | On modal characterisation theorems over finite structures with applications to graph neural networks |
| title_full | On modal characterisation theorems over finite structures with applications to graph neural networks |
| title_fullStr | On modal characterisation theorems over finite structures with applications to graph neural networks |
| title_full_unstemmed | On modal characterisation theorems over finite structures with applications to graph neural networks |
| title_short | On modal characterisation theorems over finite structures with applications to graph neural networks |
| title_sort | on modal characterisation theorems over finite structures with applications to graph neural networks |
| work_keys_str_mv | AT pflugermf onmodalcharacterisationtheoremsoverfinitestructureswithapplicationstographneuralnetworks |