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 proceedingArticle in proceedingsResearchpeer-review

    21 Downloads (Pure)

    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 languageEnglish
    Title of host publicationInternational Symposium on Formal Techniques in Real-Time and Fault-Tolerant systems (FTRTFT 2002)
    PublisherSpringer
    Publication date2002
    Pages245-264
    Publication statusPublished - 2002

    Fingerprint Dive into the research topics of 'Take it NP-easy: Bounded model construction for duration calculus'. Together they form a unique fingerprint.

    Cite this