论文部分内容阅读
古典逻辑不能被用来有效地与矛盾关于并发的系统推理(矛盾经常发生特别在发展的早阶段，当大、复杂的并发的系统被开发时) 。在这份报纸，甚至在历久不渝的模型不是可得到的的地方，我们为支持如此的系统的时间的性质的确认建议 guasi 古典的时间的逻辑(QCTL ) 的使用。我们的模型是 paraKripke 结构(扩大标准 Kripke 结构) ，在哪个一个公式和它的否定处于一个一样的状态满足，并且要验证的性质被 QCTL 与 paraKripke 结构表示语义。我们介绍 paraKripke 模型的一个新奇观点