0483809 - ÚI 2023 RIV DE eng J - Článek v odborném periodiku
Bílková, Marta - Dostál, M.
Moss' Logic for Ordered Coalgebras.
Logical Methods in Computer Science. Roč. 18, č. 3 (2022), 18:1-18:61. ISSN 1860-5974. E-ISSN 1860-5974
Grant CEP: GA ČR(CZ) GC16-07954J
Grant ostatní: GA ČR(CZ) GPP202/11/P304
Institucionální podpora: RVO:67985807
Klíčová slova: coalgebraic logic * cover modality * relation lifting * ordered coalgebras * similarity * Hennessy-Milner property
Obor OECD: Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Impakt faktor: 0.6, rok: 2022 ; AIS: 0.437, rok: 2022
Způsob publikování: Open access
Web výsledku:
https://dx.doi.org/10.46298/lmcs-18(3:18)2022DOI: https://doi.org/10.46298/lmcs-18(3:18)2022

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∂ω, 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∂ω is required to preserve finite intersections. We develop a notion of a base for subobjects of Tω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.
Trvalý link: http://hdl.handle.net/11104/0278984