HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Duality for Instantial Neighbourhood Logic via Coalgebra

Abstract : Instantial Neighbourhood Logic (INL) has been introduced recently as a language for neighbourhood frames where existential information can be given about what kind of worlds occur in a neighbourhood of a current world. Apart from its semantics, its proof theory and bisimulation games have also been studied. However, conspicuously absent from the treatment of INL is the notion of descriptive frames.This is the gap that we are closing in this paper. We introduce descriptive frames for INL and we prove that these are dual to boolean algebras with instantial operators (BAIOs), which give the algebraic semantics of INL. Our methods for establishing this duality make essential use of coalgebra: we observe that BAIOs are algebras for a functor on the category of boolean algebras and show that this functor is dual to the double Vietoris functor (i.e. the composition of the Vietoris functor with itself), thus obtaining a dual equivalence between double Vietoris coalgebras and BAIOs. The proof of our main result is then completed by showing that double Vietoris coalgebras correspond precisely to descriptive frames. As a corollary we obtain that every extension of INL is sound and complete with respect to descriptive frames, that descriptive frames enjoy the Hennessy-Milner property, and as a result, that finite neighbourhood frames enjoy the Hennessy-Milner property.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03232350
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, May 21, 2021 - 2:57:53 PM
Last modification on : Thursday, February 24, 2022 - 1:38:04 PM
Long-term archiving on: : Sunday, August 22, 2021 - 6:49:07 PM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Nick Bezhanishvili, Sebastian Enqvist, Jim Groot. Duality for Instantial Neighbourhood Logic via Coalgebra. 15th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2020, Dublin, Ireland. pp.32-54, ⟨10.1007/978-3-030-57201-3_3⟩. ⟨hal-03232350⟩

Share

Metrics

Record views

19