The
Timed Concurrent
Constraint
programming language (tccp) introduces time aspects into the Concurrent
Constraint paradigm. This makes tccp especially appropriate to analyze
by model checking timing properties of concurrent systems. However,
even if very compact state representations are obtained thanks to the
use of constraints in tccp, large state spaces can be still generated
which may prevent model checking tools from verifying tccp programs
completely. In this paper, we introduce an abstract methodology which
is based on over- and under-approximating tccp models and mitigates the
state explosion problem which is common to traditional model checking
algorithms. We ascertain the conditions for the correctness of the
abstract technique and show that, due to the timing aspects of the
language, this semantics does not correctly simulate the suspension
behavior, which is a key feature of tccp. Then, we present a refined
abstract semantics which correctly models suspension.