论文标题
Hennessy-Milner定理通过Galois Connections
Hennessy-Milner Theorems via Galois Connections
论文作者
论文摘要
我们介绍了一个一般而简单的框架，使我们能够为表征行为等价或指标的模态逻辑得出合理性和表达性结果（也称为Hennessy-Milner定理）。它基于一方面（真实价值）谓词的集合之间的连接，另一方面是等效关系/指标，并涵盖了线性时间分支时间频谱的一部分，包括定性案例（行为等价）和定量案例（行为指标）。我们从给定的逻辑中得出行为函数，并提供一个称为兼容性的条件，该条件在于条件下逻辑诱导的等价/度量的条件是由fixpoint方程诱导的。特别地，此框架使我们能够得出有向跟踪指标的新固定点表征。
We introduce a general and compositional, yet simple, framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular this framework allows us to derive a new fixpoint characterization of directed trace metrics.
