A practical approach to model checking Duration Calculus using Presburger Arithmetic

作者：Hansen Michael R^*; Anh Dung Phan; Brekling Aske W

来源：Annals of Mathematics and Artificial Intelligence, 2014, 71(1-3): 251-278.

DOI：10.1007/s10472-013-9373-7

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

This paper investigates the feasibility of reducing a model-checking problem K aS aEuro parts per thousand I center dot 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 Franzle and Hansen (Int J Softw Inform 3(2-3):171-196, 2009) produces Presburger formulas whose sizes grow exponentially in the chop-depth of I center dot, 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.

• 出版日期2014-7