Hansen, Michael Reichhardt1; Dung, Phan Anh3; Brekling, Aske Wiid3
1 Department of Applied Mathematics and Computer Science, Technical University of Denmark2 Embedded Systems Engineering, Department of Applied Mathematics and Computer Science, Technical University of Denmark3 Department of Informatics and Mathematical Modeling, Technical University of Denmark
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.
Annals of Mathematics and Artificial Intelligence, 2014, Vol 71, Issue 1-3, p. 251-278
Interval temporal logic; Duration Calculus; Model checking; Presburger Arithmetic