IDLVALID : Model Checking Dense Time Duration Calculus Formulae. Duration Calculus is a dense time interval temporal logic with constructs which allow measurement of amount of time for which a proposition holds in a time interval. Interval Duration Logic is its variant where models are finite timed state sequences. An number of examples illustrate the expressive abilities of these logics. While the validity of formulae in these logics is undecidable, for practical applicability there has been considerable interest in finding techniques and tools for validity and model checking of formulae of these logics. However, there are very few available tools implementing these approaches.