Bisimulations for coalgebras on Stone spaces
| Autor: | Sumit Sourabh, Sebastian Enqvist |
|---|---|
| Přispěvatelé: | IvI Research (FNWI) |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Discrete mathematics
Bisimulation Functor Logic Computation Coalgebra Ultrafilter Modal logic 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences Theoretical Computer Science Algebra Monotone polygon Arts and Humanities (miscellaneous) 010201 computation theory & mathematics Hardware and Architecture 0202 electrical engineering electronic engineering information engineering Equivalence (formal languages) Software Mathematics |
| Zdroj: | Journal of Logic and Computation, 28(6), 991-1010. Oxford University Press |
| ISSN: | 1465-363X 0955-792X |
| Popis: | We introduce and study bisimulations for coalgebras on Stone spaces (Kupke et al., 2004, Theoretical Computer Science, 327, 109–134), motivated by previous work on ultrafilter extensions for coalgebras (Kupke et al., 2005, Algebra and Coalgebra in Computer Science, 263–277), bisimulations for the Vietoris functor (Bezhanishvili et al., 2010, Journal of Logic and Computation, 20, 1017–1040) and building on an idea of Gorin and Schroder (2013, Algebra and Coalgebra in Computer Science, 8089, 253–266). We provide a condition under which our notion of bisimulation gives a sound and complete proof method for behavioural equivalence, and show that it generalizes Vietoris bisimulations. Our main technical result proves that the topological closure of any bisimulation between Stone coalgebras in our sense is still a bisimulation. This answers a question raised in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017–1040), and also leads to a simpler proof of the main theorem in that paper, that the topological closure of a Kripke bisimulation is a Vietoris bisimulation. As a second application of our general bisimulation concept, we study neighbourhood bisimulations on descriptive frames for monotone modal logic as they were introduced in Hansen et al. (2009, Logical Methods in Computer Science, 5, 1–38). From our general results we derive that these are sound and complete for behavioural equivalence and that the topological closure of a neighbourhood bisimulation is still a neighbourhood bisimulation, in analogy with the main result in Bezhanishvili et al. (2010, Journal of Logic and Computation, 20, 1017–1040). Finally, we apply our result to bisimulations for Stone companions of set functors as defined in Kupke et al. (2004, Theoretical Computer Science, 327, 109–134). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|