Decidability, Completeness, and Extensions of Linear Temporal Logic [PhD Thesis]

This thesis was carried out under the supervision of Prof. A. Pnueli. This research deals with decidability, completeness, and extensions of linear time temporal logic. These properties are examined first for a general class of models, that are not restricted to the execution of a specific program (general validity), and then considered for a class of models representing computations of a given program (validity over program). The research contains three main parts: the first deals with Propositional Temporal Logic (PTL), the second deals with mu-Temporal Logic (muTL), which is PTL augmented by fixpoint operators, and the third part investigates XCTL which is a version of temporal logic that explicitly refers to a running clock, in order to specify real time properties of reactive programs.