Efficient Model Checking for Duration Calculus?
Received:February 28, 2009  Revised:August 07, 2009  Download PDF
Martin Fr¨anzle1,Michael R. Hansen2. Efficient Model Checking for Duration Calculus?. International Journal of Software and Informatics, 2009,3(2):171~196
Hits: 51037
Download times: 3103
Fund:This work has been partially funded by SFB/TR 14 AVACS (German Research Council), Velux Fonden, ARTIST2 (IST-004527), MoDES (Danish Research Council 2106-05-0022) and DaNES (the Danish National Advanced Technology Foundation).
Abstract:Duration Calculus (abbreviated to DC) is an interval-based, metric-time tempo-ral logic designed for reasoning about embedded real-time systems at a high level of abstrac-tion. 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 e.cient model-checking algorithms. Mim-icking the role that a situation has in (A)CTL as the origin of a set of linear traces, we de.ne 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 re.ne 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 su.ciently accurately approximating the original one. Furthermore, when chop occurs in negative polarity only in DC formulas, we have a doubly exponential model-checking algo-rithm.
keywords:model checking  interval logics  duration calculus  branching time approxi-mation
View Full Text  View/Add Comment  Download reader



Top Paper  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号