Model-checking dense-time Duration Calculus

Martin Fränzle

    Research output: Contribution to journalJournal articleResearchpeer-review

    38 Downloads (Pure)

    Abstract

    Since the seminal work of Zhou Chaochen, M. R. Hansen, and P. Sestoft on decidability of dense-time Duration Calculus [Zhou, Hansen, Sestoft, 1993] it is well-known that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that key-press verification of implementations with respect to elaborate Duration Calculus specifications were also impossible, we show that the model property is well decidable for realistic designs which feature natural constraints on their switching dynamics. The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of actual embedded real-time systems: that of finitely variable trajectories. By analysing two suitably sparser model classes we obtain model-checking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.
    Original languageEnglish
    JournalFormal Aspects of Computing
    Volume16
    Issue number2
    Pages (from-to)121-139
    ISSN0934-5043
    Publication statusPublished - 2004

    Fingerprint Dive into the research topics of 'Model-checking dense-time Duration Calculus'. Together they form a unique fingerprint.

    Cite this