Model checking CTL*[DC]

Abstract

We define a logic called CTL*[DC] which extends CTL* with ability to specify past-time and quantitative timing properties using the formulae of Quantified Discrete-time Duration Calculus (QDDC). Alternately, we can consider CTL*[DC] as extending logic QDDC with branching and liveness. As our main result, we show a reduction of CTL*[DC] model checking problem to model checking of CTL* formulae. The reduction relies upon an automat a-theoretic decision procedure for QDDC. Moreover, it preserves the subsets CTL and LTL of CTL*. The reduction is of practical relevance as model checking of CTL* as well as its subsets CTL and LTL are well studied and even implemented into a number of tools. We briefly discuss an implementation of a model checking tool for CTL [DC] called CTLDC, based on the above theory. CTLDC can model check SMV, Ver-ilog and Esterel designs using tools SMV, VIS and Xeve, respectively. © Springer-Verlag Berlin Heidelberg 2001.