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.
| Original language | English |
|---|---|
| Title of host publication | International Symposium on Formal Techniques in Real-Time and Fault-Tolerant systems (FTRTFT 2002) |
| Publisher | Springer |
| Publication date | 2002 |
| Pages | 245-264 |
| Publication status | Published - 2002 |