Interval Logics are often very expressive logics
for which decision and model-checking algorithms are hard or
even impossible to achieve, and this also applies for Duration
Calculus, which adds the notion of accumulated duration to
the Interval Temporal Logic introduced by Moszkowski et al.
In this ongoing work, we report on our experiences with implementing
the model-checking algorithm in , which reduces
model checking to checking formulas of Presburger arithmetic.
The model-checking algorithm generates Presburger formulas
that may have sizes being exponential in the chop depth of the
Duration Calculus formulas, so it is not clear whether this is
a feasible approach.
The decision procedure is partitioned into a frontend with reductions
including ”cheap”, equation-based quantifier eliminations,
and a general quantifier-elimination procedure, where we
have experimented with an implementation based on Cooper’s
algorithm and with the SMT solver Z3. The formula reductions
are facilitated using a new ’guarded normal form’. Applying
the frontend before a general quantifier elimination procedure
gave significant improvements for most of the experiments.
|Title||2011 Eighteenth International Symposium on Temporal Representation and Reasoning (TIME)|
|Conference||18th International Symposium on Temporal Representation and Reasoning|
|Period||12/09/11 → 14/09/11|