Bounded Model-checking of Discrete Duration Calculus ∗

Fränzle and Hansen investigated the model-checking problem of the subset of Duration Calculus without individual variables and quantifications w.r.t. some approximation semantics by reduction to the decision problem of Presburger Arithmetic, thus obtained a model-checking algorithm with 4-fold exponential complexity [6, 7]. As an alternative, inspired by their work, we consider the bounded model-checking problem of the subset in the context of the standard discrete-time semantics in this paper. Based on our previ-ous work [20], we reduce this problem to the reachability problem of timed automata. The complexity of our approach is singly ex-ponential in the size of formulas and quadratic in the number of states of models. We implement our approach using UPPAAL and demonstrate its efficiency by some examples