| 摘要: |
| 在PTL(propositional temporal logic)上加入一个U算子的自然拓广一2分划算子，便导出Wolper—Vardi—Sistla之ETL(extend PTL)的一个完全的子逻辑．它有更简洁的语法及公理系统、更好的判定算法等，是研究有限状态并发程序的一种理想的规范语言． |
| 关键词: 分划算子，ETL，公理演绎系统，判定复杂性，Tableau方法． |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金资助. |
|
| PARTITION EXTENSIONS OF PROPOSlTIONAL TEMPORAL LOGIC |
|
Shen Enshao
|
| Abstract: |
| Augmenting PTL(propositional temporal logic)with a 2—partition operator,which is a natural generalization of unless operator，leads to a simple but complete frag-ment of Wolper—Vardi—Sistla's ETL(extend PTL)．It has succinct deductive system，better decision algorithm，easy translation to ETL，and is an ideal specification formalism for finite—state concurrent programs． |
| Key words: Partition operator,extend PTL,deductive system,complexity of decision problem,Tableaux method． |
