Modular construction of complete coalgebraic logics
Modular construction of complete coalgebraic logics
复制标题
DOI：
10.1016/j.tcs.2007.06.002
复制
发表时间：
2007-12-05
影响因子：
1.1
通讯作者：
Pattinson, Dirk
中科院分区：
文献类型：
--
作者：
Cirstea, Corina;Pattinson, Dirk
我们提出了一种模块化的方法来定义各种基于状态的系统的逻辑。系统被建模为余代数，并且我们使用模式逻辑来描述它们的可观测性质。我们证明了与这类逻辑相关的语法、语义和证明系统都可以以模块化的方式得到。此外，我们还证明了这样得到的逻辑继承了它们的构件的可靠性、完备性和表现性。我们应用这些技术为各种各样的概率系统推导出完善的、完整的和可表达的逻辑，对于这些系统，到目前为止还没有得到完全的公理化。(C)2007 Elsevier B.V.保留所有权利。
We present a modular approach to defining logics for a wide variety of state-based systems. The systems are modelled as coalgebras, and we use modal logics to specify their observable properties. We show that the syntax, semantics and proof systems associated with such logics can all be derived in a modular fashion. Moreover, we show that the logics thus obtained inherit soundness, completeness and expressiveness properties from their building blocks. We apply these techniques to derive sound, complete and expressive logics for a wide variety of probabilistic systems, for which no complete axiomatisation has been obtained so far. (C) 2007 Elsevier B.V. All rights reserved.