Hansen, Michael Reichhardt^{1}; Dung, Phan Anh^{3}; Brekling, Aske Wiid^{3}

Affiliations:

^{1} Department of Applied Mathematics and Computer Science, Technical University of Denmark^{2} Embedded Systems Engineering, Department of Applied Mathematics and Computer Science, Technical University of Denmark^{3} Department of Informatics and Mathematical Modeling, Technical University of Denmark

DOI:

10.1007/s10472-013-9373-7

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.

Type:

Journal article

Language:

English

Published in:

Annals of Mathematics and Artificial Intelligence, 2014, Vol 71, Issue 1-3, p. 251-278

Keywords:

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