传统的观点认为保持系统刻画的协调性1是并发系统开发过程基本的要求,但随着所设计并发系统的规模越来越大,功能越来越复杂,使得自始至终维持系统的协调性成为一个具有挑战性的课题。分布式的开发方式,系统信息所固有的不确定性,进一步恶化了维持系统刻画协调性的难度和代价。因此我们需要一种超越经典逻辑观念的方法学,以一种合理的方式处理含有非协调信息的系统刻画经典逻辑具有许多直觉的属性和较强的表达、推理能力,适于刻画并发系统。但由于平凡推理的缘故,含有非协调性的形式刻画无意义。基于超协调逻辑的方法学,通过把时序的观念与超协调性的方法学相结合,本文提出了一种时序逻辑QCTL（Quasi-classical temporal logic）,一方面,QCTL具有刻画并发系统时序属性的能力,另一方面,避免了非协调情形下的平凡推理问题。本文主要研究QCTL逻辑体系,包括它的语义学、证明系统及基于QCTL的模型检测问题。为了取得形式推理上的超协调性,QCTL的证明系统与经典逻辑有着显著的差别。这个证明系统是由两种不同的推理规则构成,分为分解规则和合成规则。一个具体的证明过程由分解过程和合成过程两部分组成,并且分解过程应用分解规则,合成过程应用合成规则,这样就避免了一些能导致平凡推理的证明理论。同时,我们给出了该证明系统的可靠性和完备性证明。QCTL的语义由paraKripke结构表达,它是标准Kripke结构的一种扩展。通过这种扩展,在语义层次上解开公式α和?α之间的联系,取得了语义上的超协调性,可以用于刻画、推理含有非协调信息的并发系统。经典时序逻辑的模型检测问题得到了广泛而且深入的研究,例如CTL和LTL,但由于QCTL的逻辑理论的特殊性,传统的方法学并不适用。基于
本文来源: https://www.lw50.cn/article/93874a9841c386c6d7a69957.html