Relation-changing modal operators
Relation-changing modal operators
复制标题
改变关系的模态运算符
DOI：
10.1093/jigpal/jzv020
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Guillaume Hoffmann
中科院分区：
文献类型：
--
作者：
C. Areces;Raul Fervari;Guillaume Hoffmann
我们研究动态模态操作员，可以在评估公式期间改变模型的可访问性关系。特别是，我们以能够删除，添加或交换域元素对之间的边缘的模态扩展了基本的模态语言。我们定义一个通用框架来表征这种操作。首先，我们将改变关系的模态逻辑作为经典逻辑的片段。然后，我们使用新的框架为引入的逻辑获得了合适的分配概念，并研究了它们的表现力。最后，我们表明，引入的特定操作员的模型检查问题的复杂性是PSPACE组成的，我们研究了模型检查的两个子问题：公式复杂性和程序复杂性。
We study dynamic modal operators that can change the accessibility relation of a model during the evaluation of a formula. In particular, we extend the basic modal language with modalities that are able to delete, add or swap an edge between pairs of elements of the domain. We define a generic framework to characterize this kind of operations. First, we investigate relation-changing modal logics as fragments of classical logics. Then, we use the new framework to get a suitable notion of bisimulation for the logics introduced, and we investigate their expressive power. Finally, we show that the complexity of the model checking problem for the particular operators introduced is PSpace-complete, and we study two subproblems of model checking: formula complexity and program complexity.