@MASTERSTHESIS\{IMM2005-03622,
    author       = "J. Enslev and A. Nielsen",
    title        = "Bounded Model Construction for Duration Calculus",
    year         = "2005",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Assoc. prof. Martin Franzle and Assoc. prof. Michael R. Hansen,",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/3622-full.html",
    abstract     = "In this thesis, we shall present a tool, the {BMC}/DCValidator for automatic validation of duration calculus formulas. Duration calculus ({DC} for short) is a temporal logic, i.e. a logic for reasoning about time. {DC} may be used for specifying systems at an abstract level and the purpose of the tool is to verify that the system meets certain requirements, which are also specified using {DC}. The abstractness and expressiveness of {DC} makes it well-suited for system description, but hard to verify properties by automatic means.

Our tool provides an e cient implementation of the work of [MF02] whose main idea is to translate {DC} formulas to propositional clauses or linear constraint systems, both of which may be handed over to an external solver. The timing aspects of the formulas are represented in a discrete way, and the properties of the formulas are validated within a bounded time interval, as the unbounded validation turns out to be undecidable. In some cases, it is possible to determine a bound such that bounded validity implies general validity.

The tool has been implemented with a multitude of options such as polarity optimisation and output format that allow us to experiment with the translation algorithm. Our benchmark results show that the tool has good performance in general, but that the success of the tool is extremely dependent on the implementation details of the solver."
}