This paper introduces a branching time temporal query language called Min-max CTL which is similar in syntax to the popular temporal logic, CTL. However unlike CTL, Min-max CTL can express timing queries on a timed model. We show that 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, we show 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 Artificial Intelligence © 2001, Elsevier