Reasoning about extremal properties of events

This paper deals with a branching time temporal query language called Min-max CTL which is similar in syntax to the popular temporal logic, CTL according to E. M. Clarke (1986). Min-max CTL can express timing queries on a timed model, whereas CTL is used for untimed systems. Interesting timing queries involving a combination of min and max can be expressed in Min-max CTL. While model checking using most timed temporal logics is PSPACE complete or harder described by R. Alur and T. A. Henzinger (1993) and R. Alur et al. (1993), it is shown in the work of P. Dasgupta et al. (2001) that many practical timing queries, where we are interested in the worst case or best case timings, can be answered in polynomial time by querying the system using Min-max CTL. In this paper, the syntax of Min-max CTL is extended to increase the expressive power of Min-max CTL.