@CONFERENCE\{IMM2002-01783,
    author       = "M. Fr{\"{a}}nzle",
    title        = "Take it {NP-}easy: Bounded model construction for duration calculus",
    year         = "2002",
    month        = "sep",
    keywords     = "Discrete-time Duration Calculus; Model construction; Bounded model construction; Complexity",
    pages        = "245-264",
    booktitle    = "International Symposium on Formal Techniques in Real-Time and Fault-Tolerant systems ({FTRTFT} 2002)",
    volume       = "2469",
    series       = "Lecture Notes in Computer Science",
    editor       = "Ernst-Rüdiger Olderog and Werner Damm",
    publisher    = "Springer Verlag",
    organization = "",
    address      = "",
    url          = "http://www.imm.dtu.dk/~mf/MF-TakeItNPEasy.ps.gz",
    abstract     = "Following the recent successes of bounded model-checking, we
  reconsider the problem of constructing models of discrete-time
  Duration Calculus formulae. While this problem is known to be
  non-elementary when arbitrary length models are considered
  [Hansen94], it turns out to be only {NP-}complete
  when constrained to bounded length.
  
  As a corollary we obtain that model construction is in {NP} for the
  formulae actually encountered in case studies using Duration
  Calculus, as these have a certain small-model property.
  
  First experiments with a prototype implementation of the procedures
  demonstrate a competitive performance."
}