2022/07/12 by Harsh Beohar, Beohar, Harsh, Sebastian Gurke +5
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2207.05407
openalex publication_date 2022/07/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce a general and compositional, yet simple, framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular this framework allows us to derive a new fixpoint characterization of directed trace metrics.