@InProceedings{ fraenzlehansen08,
title = {Efficient Model Checking for Duration Calculus Based on
Branching-Time Approximations},
author = {Fr{\"a}nzle, Martin and Hansen, Michael R.},
booktitle = {Proceedings of the 6th Institute of Electrical and
Electronics Engineers (IEEE) International Conferences on
Software Engineering and Formal Methods (SEFM 08)},
year = {2008},
editor = {Antonio Cerone and Stefan Gruner},
pages = {63--72},
publisher = {Institute of Electrical and Electronics Engineers (IEEE)
Computer Society Press},
abstract = {Duration Calculus (abbreviated to DC) is an intervalbased,
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. We here investigate a
similar approximation as frequently employed in model
checking situation-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 origin of a set of linear traces, we define a
branching-time counterpart to intervalbased temporal logics
building on situation pairs spanning sets of intervals.
While this branching-time interval semantics yields the
desired reduction in complexity of the modelchecking
problem, from non-elementary 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.},
access = {restricted},
bibtex = {fraenzle.sefm08.bib},
category = {Formal Methods},
conference-long={International Conferences on Software Engineering and
Formal Methods},
conference-short={SEFM},
cross-site = { },
pdf = {fraenzle.sefm08.pdf},
subproject = {R1}
}