Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras
arxiv(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要