论文部分内容阅读
在ＰＴＬ（ｐｒｏｐｏｓｉｔｉｏｎａｌ ｔｅｍｐｏｒａｌ ｌｏｇｉｃ）上加入一个Ｕ算子的自然拓广－２分划算子，便导出了Ｗｏｌｐｅｒ－Ｖａｒｄｉ－Ｓｉｓｔｌａ之ＥＴＬ（ｅｘｔｅｎｄ ＰＴＬ）的一个完全的子逻辑，它有更简洁的语法及公理系统、更好地判定算法等，是研究有限状态并发程序的一种理想的规范语言。