Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

التفاصيل البيبلوغرافية
العنوان: Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach
المؤلفون: Beohar, Harsh, Gurke, Sebastian, König, Barbara, Messing, Karla, Forster, Jonas, Schröder, Lutz, Wild, Paul
سنة النشر: 2023
المجموعة: Computer Science
مصطلحات موضوعية: Computer Science - Logic in Computer Science
الوصف: We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances).
نوع الوثيقة: Working Paper
URL الوصول: http://arxiv.org/abs/2310.05711
رقم الأكسشن: edsarx.2310.05711
قاعدة البيانات: arXiv