On Tool Support for Duration Calculus on the Basis of Presburger Arithmetic

Michael Reichhardt Hansen, Aske Wiid Brekling

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    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.
    Original languageEnglish
    Title of host publication2011 Eighteenth International Symposium on Temporal Representation and Reasoning (TIME)
    PublisherIEEE
    Publication date2011
    Pages115-122
    ISBN (Print)978-1-4577-1242-5
    DOIs
    Publication statusPublished - 2011
    Event18th International Symposium on Temporal Representation and Reasoning - Lübeck, Germany
    Duration: 12 Sep 201114 Sep 2011
    Conference number: 18
    http://www.isp.uni-luebeck.de/time11/

    Conference

    Conference18th International Symposium on Temporal Representation and Reasoning
    Number18
    CountryGermany
    CityLübeck
    Period12/09/201114/09/2011
    Internet address
    SeriesInternational Symposium on Temporal Representation and Reasoning. Proceedings
    ISSN1530-1311

    Fingerprint Dive into the research topics of 'On Tool Support for Duration Calculus on the Basis of Presburger Arithmetic'. Together they form a unique fingerprint.

    Cite this