命题时态逻辑的分划式扩充

在ptl(propositionaltemporallogic)上加入一个u算子的自然拓广一2分划算子，便导出wolper—vardi—sistla之etl(extendptl)的一个完全的子逻辑．它有更简洁的语法及公理系统、更好的判定算法等，是研究有限状态并发程序的一种理想的规范语言．