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

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