Take it NP-easy: Bounded model construction for duration calculus

Martin Fränzle; Ernst-Rüdiger Olderog

Take it NP-easy: Bounded model construction for duration calculus

Martin Fränzle
, Ernst-Rüdiger Olderog (Editor)

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

36 Downloads (Orbit)

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

Access to Document

Imm1783

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{57b1bd766b464a728f356929de7f7701,

title = "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",

author = "Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog",

year = "2002",

language = "English",

pages = "245--264",

booktitle = "International Symposium on Formal Techniques in Real-Time and Fault-Tolerant systems (FTRTFT 2002)",

publisher = "Springer",

}

TY - GEN

T1 - Take it NP-easy: Bounded model construction for duration calculus

AU - Fränzle, Martin

A2 - Olderog, Ernst-Rüdiger

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

KW - Discrete-time Duration Calculus; Model construction; Bounded model construction; Complexity

M3 - Article in proceedings

SP - 245

EP - 264

BT - International Symposium on Formal Techniques in Real-Time and Fault-Tolerant systems (FTRTFT 2002)

PB - Springer

ER -

Take it NP-easy: Bounded model construction for duration calculus

Abstract

Access to Document

OpenUrl availability

Fingerprint

Cite this