Min-max Computation Tree Logic (Q5940962)

This paper introduces a branching time temporal query language called Min-max CTL which is similar in syntax to the popular temporal logic, CTL [\textit{E. M. Clarke, E. A. Emerson} and \textit{A. P. Sistla}, ACM Trans. Program. Lang. Systems 8, 244-263 (1986; Zbl 0591.68027)]. 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 [\textit{R. Alur} and \textit{T. A. Henzinger}, Inf. Comput. 104, No. 1, 35-77 (1993; Zbl 0791.68103); \textit{A. Alur, C. Courcoubetis} and \textit{D. Dill}, Inf. Comput. 104, No. 1, 2-34 (1993; Zbl 0783.68076)], 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.