Model-checking dense-time duration calculus |
|
| 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. |
| Keywords | Dense-time Duration Calculus; Decidability; Model-Checking |
| Type | Journal paper [With referee] |
| Journal | Formal Aspects of Computing |
| Year | 2004 Vol. 16 No. 2 pp. 121-139 |
| Electronic version(s) | [ps] |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |