This paper presents a modified version of temporal logics for the specification and verification of reactive systems．It includes a mechanism tO explicitly distinguish pro-gram steps from environment steps and the characteristics of the environment can be taken into account during the development of system．A compositional computation model of programs——modular transition system is firstly given．Then based on this model，a mod-ified temporal logic and its proof rules are presented．The proposed approach is used with-in Manna-Pnueli'S temporal logic framework．The classical example of the Resource Allo-cator is used tO illustrate the approach．At the end of the paper，a parallel composition principle is proposed，it can be viewed as an application of Abadi and Lamport'S works on the composing assumption/guarantee specifications．