A MODIFIED TEMPORAL LOGIC FOR REACTIVE SYSTEMS
用于反应系统的修改时序逻辑

This paper presents a modified version of ternporal logics for the specificationand verification of reactive systems. It includes a mechanism to explicitly distinguish pro-gram steps from environment steps and the characteristics of the erivironment can be takeninto account during the development of system. A cornpositional computation model ofprograrns-modular transition system is firstly given. Then based on this model, a mod-if ied temporal logic and its proof rules are presented. The proposed approach is used with-in Manna-Pnueli's ternporal logic framework. The classical example of the Resource Allo-cator is used to illustrate the approach. At the end of the paper, a parallel compositionprinciple is proposed, it can be viewed as an application of Abadi and Lamport's works onthe composing assurnption/guarantee specifications.