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

翻译：我们解决了从刻画行为等价性和度量（统称为一致性）的模态逻辑中推导不动点方程的问题。我们基于先前的工作，该工作通过合适格之间的伽罗瓦连接上的不动点保持性质，将Hennessy-Milner定理作为推论导出。我们将此实例化到余代数的设定中，在其中详细阐述了兼容性性质，确保我们能推导出一个行为函数，其最大不动点与逻辑一致性一致。随后我们专注于线性时间情形，研究基于生活在Eilenberg-Moore范畴中的机器函子的余代数，在此场景下我们得到了一个特别简单的逻辑和不动点方程。该理论被实例化到具体案例中，既包括分支时间情形（互模拟等价性和行为度量），也包括线性时间情形（迹等价性和迹距离）。