论文标题
共同感应谓词的表达逻辑
Expressive Logics for Coinductive Predicates
论文作者
论文摘要
经典的轩尼诗 - 米勒纳（Hennessy-Milner Theorem）说，只有在某个模态逻辑中满足相同的公式时，图像 - 限制过渡系统的两个状态是偶然的。在本文中，我们在一般环境中研究了这种类型的结果，从过渡系统转变为山结构，从双性恋到共同诱导谓词。我们通过提供适当的充分性和表现力的概念，并在语义上提供足够的条件来表达逻辑何时完全表征了山结构上的共同感应谓词。该方法以表征相似性，差异和自动机的行为度量的逻辑进行说明。
The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.
