空间逻辑的一个定义框架及其可判定性  

A Definition Framework of Spatial Logic and Decidability

作　　者：颜锋[1] 陈韬略[1] 韩婷婷[1] 吕建[1] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,南京210093

出　　处：《计算机科学》2006年第6期7-10,共4页Computer Science

基　　金：国家重点基础研究发展规划973项目(2002CB312002);863项目(2002AA116010);国家自然科学基金(60273034)。

摘　　要：空间逻辑作为一个模态逻辑,能很好地描述分布式系统的行为和空间属性。其中,逻辑公式的有效性、可满足性及模型检测问题的可判定性已经得到广泛的研究。本文即是关于空间逻辑可判定性的一个综述,为此首先提出一个空间逻辑的定义框架,据此可以构造各种空间逻辑,并对它们的可判定性进行考察,从而指出影响空间逻辑的可判定性的关键因素。The introduction of spatial logics has been motivated by a recent shift of focus from monolithic concurrent systems towards distributed computing systems. The decidability of validity, satisfiability,and model checking for spa tial logics is an important issue which has been studied deeply. This paper is survey of these results. For this,a defini tion framework of spatial logic is proposed for constructing various logics and the decidability is investigated. And the crux of the matter that influences the decidability of spatial logics is revealed.

关 键 词：移动计算 分布式计算 空间逻辑 可判定性 定义框架 

分 类 号：TP31[自动化与计算机技术—计算机软件与理论]