Take it NP-easy: bounded model construction for duration calculus. (English) Zbl 1278.68170
Damm, Werner (ed.) et al., Formal techniques in real-time and fault-tolerant systems. 7th international symposium, FTRTFT 2002, co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 9–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-44165-4/pbk). Lecture Notes in Computer Science 2469, 245-264 (2002).
Summary: 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, 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.
For the entire collection see [Zbl 1045.68008].
For the entire collection see [Zbl 1045.68008].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
