Take it NP-easy: Bounded model construction for duration calculus |
|
| 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. |
| Keywords | Discrete-time Duration Calculus; Model construction; Bounded model construction; Complexity |
| Type | Conference paper [With referee] |
| Conference | International Symposium on Formal Techniques in Real-Time and Fault-Tolerant systems (FTRTFT 2002) |
| Editors | |
| Year | 2002 Month September Vol. 2469 pp. 245-264 |
| Publisher | Springer Verlag |
| Series | Lecture Notes in Computer Science |
| Electronic version(s) | [ps] |
| Publication link | http://www.imm.dtu.dk/~mf/MF-TakeItNPEasy.ps.gz |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |