Duality for Logics of Transition Systems
Duality for Logics of Transition Systems
复制标题
转移系统逻辑的对偶性
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
A. Kurz
中科院分区：
文献类型：
--
作者：
M. Bonsangue;A. Kurz
我们提出了一个通用的框架逻辑的基础上石对偶的过渡系统。转移系统被建模为范畴χ上函子T的余代数。用于从χ推理状态空间的命题逻辑由χ的Stone对偶${\mathcal A}$建模（例如，如果χ是Stone空间，则${\mathcal A}$是布尔代数，命题逻辑是经典的）。为了获得转移系统（即T-余代数）的模态逻辑，我们考虑${\mathcalA}$上与T对偶的函子L。通过构造，得到了T-余代数的一个充分模态逻辑，它与T-余代数的范畴是对偶的.对偶性的逻辑意义是，逻辑是健全的、完整的和表达的（或完全抽象的），在这个意义上，非双相似的状态由某种公式区分。
我们应用的框架，拓扑空间上的Vietoris余代数，利用空间和观察框架之间的对偶，以获得足够的逻辑偏序集，集，谱空间和斯通空间上的过渡系统。
We present a general framework for logics of transition systems based on Stone duality. Transition systems are modelled as coalgebras for a functor T on a category χ. The propositional logic used to reason about state spaces from χ is modelled by the Stone dual ${\mathcal A}$ of χ (e.g. if χ is Stone spaces then ${\mathcal A}$ is Boolean algebras and the propositional logic is the classical one). In order to obtain a modal logic for transition systems (i.e. for T-coalgebras) we consider the functor L on ${\mathcal A}$ that is dual to T. An adequate modal logic for T-coalgebras is then obtained from the category of L-algebras which is, by construction, dual to the category of T-coalgebras. The logical meaning of the duality is that the logic is sound and complete and expressive (or fully abstract) in the sense that non-bisimilar states are distinguished by some formula.
We apply the framework to Vietoris coalgebras on topological spaces, using the duality between spaces and observation frames, to obtain adequate logics for transition systems on posets, sets, spectral spaces and Stone spaces.