On compositionality and its limitations
On compositionality and its limitations
复制标题
论组合性及其局限性
DOI：
10.1145/1182613.1182617
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
A. Rabinovich
中科院分区：
文献类型：
--
作者：
A. Rabinovich
本文的目的是检验由Feferman和Vaught提出的广义积构造的合成方法在程序验证领域的适用性，给出了广义积构造的一个实例，并证明了模态逻辑的一个合适的合成定理。我们说明了这种广义产品的有用性，通过显示，许多“并行组合”操作是这种广义产品的特殊情况下，我们得到了积极的结果（组合方法的作品）的基本命题模态逻辑，和消极的结果（组合方法失败），更有表现力的逻辑，可以表示EGp---“有一条路径，使所有的节点的路径具有属性p”。复合定理的模型检验问题和参数模型检验问题的应用。
The aim of this article is to examine the applicability of a compositional method developed for a generalized product construction by Feferman and Vaught to the field of program verification.We suggest an instance of the generalized product construction and prove an appropriate composition theorem for modal logic. We illustrate the usefulness of this generalized product by showing that many “parallel composition” operations are special cases of this generalized product.We obtain positive results (the compositional method works) for basic propositional modal logic, and negative results (the compositional method fails) for more expressive logics which can express EGp---“there is a path such that all the nodes of the path have the property p.”Applications of the composition theorem to the model-checking problem and to the parametric model-checking problem are provided.