Min-max computation tree logic

Abstract

This paper introduces a branching time temporal query language called Min-max CTL which is similar in syntax to the popular temporal logic, CTL [Clarke et al., ACM Trans. Program. Lang. Systems 8 (1986) 244]. 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 [Alur and Henzinger, Inform. and Comput. 104 (1993) 35; Alur et al., Inform. and Comput. 104 (1993) 2], 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.