### Abstract

Original language | English |
---|---|

Journal | Annals of Mathematics and Artificial Intelligence |

Volume | 71 |

Issue number | 1-3 |

Pages (from-to) | 251-278 |

ISSN | 1012-2443 |

DOIs | |

Publication status | Published - 2014 |

### Keywords

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

### Cite this

*Annals of Mathematics and Artificial Intelligence*,

*71*(1-3), 251-278. https://doi.org/10.1007/s10472-013-9373-7

}

*Annals of Mathematics and Artificial Intelligence*, vol. 71, no. 1-3, pp. 251-278. https://doi.org/10.1007/s10472-013-9373-7

**A practical approach to model checking Duration Calculus using Presburger Arithmetic.** / Hansen, Michael Reichhardt; Dung, Phan Anh; Brekling, Aske Wiid.

Research output: Contribution to journal › Journal article › Research › peer-review

TY - JOUR

T1 - A practical approach to model checking Duration Calculus using Presburger Arithmetic

AU - Hansen, Michael Reichhardt

AU - Dung, Phan Anh

AU - Brekling, Aske Wiid

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Interval temporal logic

KW - Duration Calculus

KW - Model checking

KW - Presburger Arithmetic

U2 - 10.1007/s10472-013-9373-7

DO - 10.1007/s10472-013-9373-7

M3 - Journal article

VL - 71

SP - 251

EP - 278

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 1-3

ER -