Suitability of the propositional temporal logic to express properties of real-time systems

Abstract

We claim in this paper that the Propositional Temporal Logic (PTL) is an adequate logic to specify a reactive system. To prove this affirmation, we present abbreviations which allow the expression of the most important real-time properties and some other important requirements. We show that they are easy to use and that the induced complexity cost is the same as the complexity of the other real-time logics. Finally, we prove that many real-time logics already published have exactly the same expressive power as PTL.