@Article{ fraenzlehansen:branchingtimedcjournal,
title = {Efficient Model Checking for Duration Calculus},
author = {Martin Fr{\"a}nzle and Hansen, Michael R.},
journal = {International Journal of Software and Informatics},
year = {2009},
number = {2--3},
pages = {171--196},
volume = {3},
abstract = {Duration Calculus (abbreviated to DC) is an
interval-based, metric-time temporal logic designed for
reasoning about embedded real-time systems at a high level
of abstraction. But the complexity of model checking any
decidable fragment featuring both negation and chop,
DCâ€™s only modality, is non-elementary and thus
impractical. Even worse, when such decidable fragments are
generalized just slightly to cover more interesting
durational constraints the resulting fragments become
undecidable. We here investigate a similar approximation as
frequently employed in model checking situation- or
point-based temporal logics, where linear-time problems are
safely approximated by branching-time counterparts amenable
to more efficient model-checking algorithms. Mimicking the
role that a situation has in (A)CTL as the origin of a set
of linear traces, we define a branching-time counterpart to
interval-based temporal logics building on situation pairs
spanning sets of intervals. While this branching-time
interval semantics yields the desired reduction in
complexity of the model-checking problem, from undecidable
to linear in the size of the formula and cubic in the size
of the model, the approximation is too coarse to be
practical. We therefore refine the semantics by an
occurrence count for crucial states (e.g., cuts of loops)
in the model, arriving at a 4-fold exponential
model-checking problem sufficiently accurately
approximating the original one. Furthermore, when chop
occurs in negative polarity only in DC formulas, we have a
doubly exponential model-checking algorithm.},
access = {restricted},
bibtex = {fraenzle.ijsi09.bib},
category = {other},
cross-site = { },
pdf = {fraenzle.ijsi09.pdf},
journal-long = {International Journal of Software and Informatics},
journal-short = {IJSI},
subproject = {R1}
}