A practical approach to model checking Duration Calculus using Presburger Arithmetic

Michael Reichhardt Hansen, Phan Anh Dung, Aske Wiid Brekling

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

This paper investigates the feasibility of reducing a model-checking problem K ⊧ ϕ for discrete time Duration Calculus to the decision problem for Presburger Arithmetic. Theoretical results point at severe limitations of this approach: (1) the reduction in Fränzle and Hansen (Int J Softw Inform 3(2–3):171–196, 2009) produces Presburger formulas whose sizes grow exponentially in the chop-depth of ϕ, where chop is an interval modality originating from Moszkowski (IEEE Comput 18(2):10–19, 1985), and (2) the decision problem for Presburger Arithmetic has a double exponential lower bound and a triple exponential upper bound. The generated Presburger formulas have a rich Boolean structure, many quantifiers and quantifier alternations. Such formulas are simplified using so-called guarded formulas, where a guard provides a context used to simplify the rest of the formula. A normal form for guarded formulas supports global effects of local simplifications. Combined with quantifier-elimination techniques, this normalization gives significant reductions in formula sizes and in the number of quantifiers. As an example, we solve a configuration problem using the SMT-solver Z3 as backend. Benefits and the current limits of the approach are illustrated by a family of examples.
Original languageEnglish
JournalAnnals of Mathematics and Artificial Intelligence
Volume71
Issue number1-3
Pages (from-to)251-278
ISSN1012-2443
DOIs
Publication statusPublished - 2014

Keywords

  • Interval temporal logic
  • Duration Calculus
  • Model checking
  • Presburger Arithmetic

Fingerprint Dive into the research topics of 'A practical approach to model checking Duration Calculus using Presburger Arithmetic'. Together they form a unique fingerprint.

Cite this