Number of the records: 1
Fixed Point Logics on Hemimetric Spaces
- 1.
SYSNO ASEP 0574237 Document Type C - Proceedings Paper (int. conf.) R&D Document Type Conference Paper Title Fixed Point Logics on Hemimetric Spaces Author(s) Fernández-Duque, David (UIVT-O) SAI, ORCID, RID
Gougeon, Q. (FR)Number of authors 2 Article number 190687 Source Title 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) Proceedings. - New York : IEEE, 2023 - ISBN 979-8-3503-3588-0 Number of pages 13 s. Publication form Print - P Action LICS 2023: Annual ACM/IEEE Symposium on Logic in Computer Science /38./ Event date 26.06.2023 - 29.06.2023 VEvent location Boston Country US - United States Event type WRD Language eng - English Country US - United States Keywords Computer science ; Semantics ; Extraterrestrial measurements ; Behavioral sciences ; Proposals ; Standards OECD category Pure mathematics R&D Projects GA22-01137S GA ČR - Czech Science Foundation (CSF) Institutional support UIVT-O - RVO:67985807 UT WOS 001036707700049 EID SCOPUS 85165985774 DOI https://doi.org/10.1109/LICS56636.2023.10175784 Annotation The μ-calculus can be interpreted over metric spaces and is known to enjoy, among other celebrated properties, variants of the McKinsey-Tarski completeness theorem and of Dawar and Otto's modal characterization theorem. In its topological form, this theorem states that every topological fixed point may be defined in terms of the tangled derivative, a polyadic generalization of Cantor's perfect core. However, these results fail when spaces not satisfying basic separation axioms are considered, in which case the base modal logic is not the well-known K4, but the weaker wK4.In this paper we show how these shortcomings may be overcome. First, we consider semantics over the wider class of hemimetric spaces, and obtain metric completeness results for wK4 and related logics. In this setting, the Dawar-Otto theorem still fails, but we argue that this is due to the tangled derivative not being suitably defined for general application in arbitrary topological spaces. We thus introduce the hybrid tangle, which coincides with the tangled derivative over metric spaces but is better behaved in general. We show that only the hybrid tangle suffices to define simulability of finite structures, a key 'test case' for an expressively complete fragment of the μ-calculus. Workplace Institute of Computer Science Contact Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800 Year of Publishing 2024 Electronic address https://dx.doi.org/10.1109/LICS56636.2023.10175784
Number of the records: 1