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

Cite this

@article{f96fe939808343c8bd7fe9e865958eed,
title = "A practical approach to model checking Duration Calculus using Presburger Arithmetic",
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{\"a}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.",
keywords = "Interval temporal logic, Duration Calculus, Model checking, Presburger Arithmetic",
author = "Hansen, {Michael Reichhardt} and Dung, {Phan Anh} and Brekling, {Aske Wiid}",
year = "2014",
doi = "10.1007/s10472-013-9373-7",
language = "English",
volume = "71",
pages = "251--278",
journal = "Annals of Mathematics and Artificial Intelligence",
issn = "1012-2443",
publisher = "Springer Netherlands",
number = "1-3",

}

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

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

Research output: Contribution to journalJournal articleResearchpeer-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 -