Marta Bílková ; Matěj Dostál - Moss' logic for ordered coalgebras

lmcs:5158 - Logical Methods in Computer Science, August 9, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:18)2022
Moss' logic for ordered coalgebrasArticle

Authors: Marta Bílková ; Matěj Dostál

    We present a finitary version of Moss' coalgebraic logic for $T$-coalgebras, where $T$ is a locally monotone endofunctor of the category of posets and monotone maps. The logic uses a single cover modality whose arity is given by the least finitary subfunctor of the dual of the coalgebra functor $T_\omega^\partial$, and the semantics of the modality is given by relation lifting. For the semantics to work, $T$ is required to preserve exact squares. For the finitary setting to work, $T_\omega^\partial$ is required to preserve finite intersections. We develop a notion of a base for subobjects of $T_\omega X$. This in particular allows us to talk about the finite poset of subformulas for a given formula. The notion of a base is introduced generally for a category equipped with a suitable factorisation system. We prove that the resulting logic has the Hennessy-Milner property for the notion of similarity based on the notion of relation lifting. We define a sequent proof system for the logic, and prove its completeness.


    Volume: Volume 18, Issue 3
    Published on: August 9, 2022
    Accepted on: May 13, 2022
    Submitted on: February 1, 2019
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1936 times.
    This article's PDF has been downloaded 555 times.