Coalgebra, as the abstract study of state-based systems, comes naturally equipped with a notion of behavioural equivalence that identifies states exhibiting the same behaviour. In many cases, however, this equivalence is finer than the intended semantics. Particularly in automata theory, behavioural equivalence of nondeterministic automata is essentially bisimilarity, and thus does not coincide with language equivalence. Language equivalence can be captured as behavioural equivalence on the determinization, which is obtained via the standard powerset construction. This construction can be lifted to coalgebraic generality, assuming a so-called Eilenberg-Moore distributive law between the functor termining the type of accepted structure (e.g.\ word languages) and a monad capturing the branching type (e.g.\ nondeterministic, weighted, probabilistic). Eilenberg-Moore-style coalgebraic semantics in this sense has been shown to be essentially subsumed by the more general framework of graded semantics, which is centrally based on graded monads. Graded semantics comes with a range of generic results, in particular regarding invariance and, under suitable conditions, expressiveness of dedicated modal logics for a given semantics; notably, these logics are evaluated on the original state space. We show that the instantiation of such graded logics to the case of Eilenberg-Moore-style semantics works extremely smoothly, and yields expressive modal logics in essentially all cases of interest. We additionally parametrize the framework over a quantale of truth values, thus in particular covering both the two-valued notions of equivalence and quantitative ones, i.e. behavioural distances.

翻译：余代数为基于状态的系统提供了抽象研究，天然地具备一种行为等价概念，能够识别表现出相同行为的状态。然而，在许多情况下，这种等价关系比预期语义更精细。特别是在自动机理论中，非确定性自动机的行为等价本质上就是互模拟等价，因此并不等同于语言等价。语言等价可通过确定性化（通过标准幂集构造获得）上的行为等价来捕捉。假设在决定所接受结构类型（例如单词语言）的函子与捕获分支类型（例如非确定性、加权、概率）的幺半群之间存在所谓的Eilenberg-Moore分配律，则该构造可提升至余代数的一般性。在此意义上，Eilenberg-Moore风格的余代数语义已被证明本质上被更一般的分级语义框架所包含，该框架以分级幺半群为核心基础。分级语义提供了一系列通用结果，特别涉及不变性以及在适当条件下针对给定语义的专用模态逻辑的表达能力；值得注意的是，这些逻辑是在原始状态空间上进行评估的。我们证明，将此类分级逻辑实例化到Eilenberg-Moore风格语义的情形能够极其平滑地工作，并在几乎所有感兴趣的情形下都能产生具有表达能力的模态逻辑。此外，我们通过一个真值量程对该框架进行参数化，从而同时涵盖了两值等价概念和定量等价概念（即行为距离）。