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).

翻译：我们致力于解决从刻画行为等价性和度量（统称为一致性）的模态逻辑中推导不动点方程的任务。我们基于此前利用伽罗瓦连接中不动点保持性质推导亨尼西-米尔纳定理的研究工作，将这一性质推广至共代数框架。在此框架下，我们详细阐述了确保能推导出行为函数的相容性条件，该行为函数的最大不动点与逻辑一致性完全吻合。随后聚焦线性时间情形，研究了基于埃伦伯格-穆尔范畴中机器函子的共代数，并为此场景获得了极简逻辑与不动点方程。该理论被具体应用于分支时间情形（双模拟等价与行为度量）和线性时间情形（迹等价与迹距离）的实例。