本文在研究了命题投影时序逻辑PPTL(Propositional Projection Temporal Logic)的语义和语法的基础上,详细阐述了它的判定过程和表达性。首先介绍了命题投影时序逻辑,包括基本的语法、语义和一些派生公式及常用逻辑等式,该逻辑除了包含有常用的逻辑操作符∨(或)和?(非)外,还包含了两个时序操作符○(next)和prj(投影操作符)。其次,本文定义了命题投影时序逻辑公式的正则形(normal form),根据公式的结构采用归纳的方法证明了任意PPTL公式都可以转换为正则形定理的正确性并且给出了相应的转换算法。该算法将所有逻辑公式都归结为一种统一的形式,这是采用Tableau方法进行判定的前提和基础。再次,为了找到给定公式的模型,本文介绍了正则图(normal form graph)的概念,给出了为PPTL公式构造正则图的算法和命题投影时序逻辑的判定过程,该方法简单实用。最后,本文介绍和比较了区间时序逻辑中两个版本的投影结构并研究了这两个投影结构的表达性,结果表明prj投影结构比原始的投影结构proj的表达性更强。