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．