Conference paper
On Tool Support for Duration Calculus on the Basis of Presburger Arithmetic
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 [12], 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.
Language: | English |
---|---|
Publisher: | IEEE |
Year: | 2011 |
Pages: | 115-122 |
Proceedings: | 18th International Symposium on Temporal Representation and Reasoning |
Series: | International Symposium on Temporal Representation and Reasoning. Proceedings |
ISBN: | 1457712423 and 9781457712425 |
ISSN: | 23326468 and 15301311 |
Types: | Conference paper |
DOI: | 10.1109/TIME.2011.26 |
ORCIDs: | Hansen, Michael Reichhardt |
Approximation methods Automata Calculus Cooper algorithm Duration calculus Interval temporal logic Mathematical model Presburger arithmetic Presburger formula Presburger srithmetic Radiation detectors SMT solver Z3 Semantics Silicon decision algorithm duration calculus equation-based quantifier elimination expressive logics formal verification formula checking interval temporal logic model checking model-checking algorithm number theory process algebra temporal logic tool support