Unified temporal logic.

• Unified Temporal Logic (UTL) is proposed which combines the characteristics of standard Linear Temporal Logic and Propositional Projection Temporal Logic. • The syntax and semantics of UTL are defined. • Logic laws in UTL are explored and some of them are semantically proved in detail. • The normal forms of UTL formulas are defined. It is also proved that each UTL formula can be equivalently transformed into a normal form. • A practical example of an elevator control system is given to show how to describe temporal properties with UTL. This paper proposes a new temporal logic named Unified Temporal Logic (UTL). First, the syntax and semantics of UTL are inductively defined. Further, logic laws in UTL are formalized and proved. Moreover, the normal forms of UTL formulas are defined and proved. To illustrate how to describe properties with UTL, an example of an elevator control system is given. In general, UTL combines the characteristics of Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). So properties involving the "until" construct in LTL and the "chop" construct in PPTL can easily be represented in UTL. In addition, both finite and infinite models (intervals) are supported. With UTL, we are able to specify and verify some practical properties which cannot easily be formalized in LTL and PPTL. [ABSTRACT FROM AUTHOR]