02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
02917 Advanced Topics in Embedded Systems Presburger Arithmetic: Cooper’s algorithm
Michael R. Hansen
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Introduction
Presburger Arithmetic(introduced by Mojzesz Presburger in 1929), is the first-order theory of natural numbers with addition.
Examples of formulas are:∃x.2x=yand∃x.∀y.x+y>z.
Unlike Peano Arithmetic, which also includes multiplication, Presburger Arithmetic is adecidable theory.
We shall consider the algorithm introduced by D.C Cooper in 1972.
The presentation is based on: Chapter 7: Quantified Linear Arithmetic of The Calculus of Computation by Bradley and Manna.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Introduction
Presburger Arithmetic(introduced by Mojzesz Presburger in 1929), is the first-order theory of natural numbers with addition.
Examples of formulas are:∃x.2x=yand∃x.∀y.x+y>z.
Unlike Peano Arithmetic, which also includes multiplication, Presburger Arithmetic is adecidable theory.
We shall consider the algorithm introduced by D.C Cooper in 1972.
The presentation is based on: Chapter 7: Quantified Linear Arithmetic of The Calculus of Computation by Bradley and Manna.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Introduction
Presburger Arithmetic(introduced by Mojzesz Presburger in 1929), is the first-order theory of natural numbers with addition.
Examples of formulas are:∃x.2x=yand∃x.∀y.x+y>z.
Unlike Peano Arithmetic, which also includes multiplication, Presburger Arithmetic is adecidable theory.
We shall consider the algorithm introduced by D.C Cooper in 1972.
The presentation is based on: Chapter 7: Quantified Linear Arithmetic of The Calculus of Computation by Bradley and Manna.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Introduction
Presburger Arithmetic(introduced by Mojzesz Presburger in 1929), is the first-order theory of natural numbers with addition.
Examples of formulas are:∃x.2x=yand∃x.∀y.x+y>z.
Unlike Peano Arithmetic, which also includes multiplication, Presburger Arithmetic is adecidable theory.
We shall consider the algorithm introduced by D.C Cooper in 1972.
The presentation is based on: Chapter 7: Quantified Linear Arithmetic of The Calculus of Computation by Bradley and Manna.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Presburger terms
Thetermsare generated from
∙ integer constants. . . ,−2,−1,0,1,2, . . .and
∙ variablesx,y,z, . . . using the followingoperations:
∙ addition+and subtraction−and
∙ multiplication by constants:. . . , −2⋅, −1⋅,0⋅,1⋅, 2⋅, . . . Notice
∙ terms are interpreted overintegers
∙ the terms do not really allow multiplication as, e.g.3⋅xis equal tox+x+x
∙ a term like3⋅xis usually written3x
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Presburger terms
Thetermsare generated from
∙ integer constants. . . ,−2,−1,0,1,2, . . .and
∙ variablesx,y,z, . . . using the followingoperations:
∙ addition+and subtraction−and
∙ multiplication by constants:. . . , −2⋅, −1⋅,0⋅,1⋅, 2⋅, . . . Notice
∙ terms are interpreted overintegers
∙ the terms do not really allow multiplication as, e.g.3⋅xis equal tox+x+x
∙ a term like3⋅xis usually written3x
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Presburger terms
Thetermsare generated from
∙ integer constants. . . ,−2,−1,0,1,2, . . .and
∙ variablesx,y,z, . . . using the followingoperations:
∙ addition+and subtraction−and
∙ multiplication by constants:. . . , −2⋅, −1⋅,0⋅,1⋅, 2⋅, . . . Notice
∙ terms are interpreted overintegers
∙ the terms do not really allow multiplication as, e.g.3⋅xis equal tox+x+x
∙ a term like3⋅xis usually written3x
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Presburger terms
Thetermsare generated from
∙ integer constants. . . ,−2,−1,0,1,2, . . .and
∙ variablesx,y,z, . . . using the followingoperations:
∙ addition+and subtraction−and
∙ multiplication by constants:. . . , −2⋅, −1⋅,0⋅,1⋅, 2⋅, . . . Notice
∙ terms are interpreted overintegers
∙ the terms do not really allow multiplication as, e.g.3⋅xis equal tox+x+x
∙ a term like3⋅xis usually written3x
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Formulas
We considerformulasF,G,F1,G1,F2. . .of the following forms:
∙ s=t,s<t,s>t,s≤t, ands≥t (comparisons)
∙ 1∣s,2∣s,3∣s, . . . (divisibility constraints)
∙ ⊤(true) and⊥(false) (propositional constants)
∙ F∨G(disjunction),F∧G(conjunction) and¬F(negation) (propositional connectives)
∙ ∃x.F(reads ”there exists anxsuch thatF”) and
∀x.F(reads ”for allx:F”) (first-order fragment) wheresandtare terms andxis a variable.
Furthermore, We allow brackets in formulas.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Formulas
We considerformulasF,G,F1,G1,F2. . .of the following forms:
∙ s=t,s<t,s>t,s≤t, ands≥t (comparisons)
∙ 1∣s,2∣s,3∣s, . . . (divisibility constraints)
∙ ⊤(true) and⊥(false) (propositional constants)
∙ F∨G(disjunction),F∧G(conjunction) and¬F(negation) (propositional connectives)
∙ ∃x.F(reads ”there exists anxsuch thatF”) and
∀x.F(reads ”for allx:F”) (first-order fragment) wheresandtare terms andxis a variable.
Furthermore, We allow brackets in formulas.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Formulas
We considerformulasF,G,F1,G1,F2. . .of the following forms:
∙ s=t,s<t,s>t,s≤t, ands≥t (comparisons)
∙ 1∣s,2∣s,3∣s, . . . (divisibility constraints)
∙ ⊤(true) and⊥(false) (propositional constants)
∙ F∨G(disjunction),F∧G(conjunction) and¬F(negation) (propositional connectives)
∙ ∃x.F(reads ”there exists anxsuch thatF”) and
∀x.F(reads ”for allx:F”) (first-order fragment) wheresandtare terms andxis a variable.
Furthermore, We allow brackets in formulas.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Formulas
We considerformulasF,G,F1,G1,F2. . .of the following forms:
∙ s=t,s<t,s>t,s≤t, ands≥t (comparisons)
∙ 1∣s,2∣s,3∣s, . . . (divisibility constraints)
∙ ⊤(true) and⊥(false) (propositional constants)
∙ F∨G(disjunction),F∧G(conjunction) and¬F(negation) (propositional connectives)
∙ ∃x.F(reads ”there exists anxsuch thatF”) and
∀x.F(reads ”for allx:F”) (first-order fragment) wheresandtare terms andxis a variable.
Furthermore, We allow brackets in formulas.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Formulas
We considerformulasF,G,F1,G1,F2. . .of the following forms:
∙ s=t,s<t,s>t,s≤t, ands≥t (comparisons)
∙ 1∣s,2∣s,3∣s, . . . (divisibility constraints)
∙ ⊤(true) and⊥(false) (propositional constants)
∙ F∨G(disjunction),F∧G(conjunction) and¬F(negation) (propositional connectives)
∙ ∃x.F(reads ”there exists anxsuch thatF”) and
∀x.F(reads ”for allx:F”) (first-order fragment) wheresandtare terms andxis a variable.
Furthermore, We allow brackets in formulas.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Formulas
We considerformulasF,G,F1,G1,F2. . .of the following forms:
∙ s=t,s<t,s>t,s≤t, ands≥t (comparisons)
∙ 1∣s,2∣s,3∣s, . . . (divisibility constraints)
∙ ⊤(true) and⊥(false) (propositional constants)
∙ F∨G(disjunction),F∧G(conjunction) and¬F(negation) (propositional connectives)
∙ ∃x.F(reads ”there exists anxsuch thatF”) and
∀x.F(reads ”for allx:F”) (first-order fragment) wheresandtare terms andxis a variable.
Furthermore, We allow brackets in formulas.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Formulas
We considerformulasF,G,F1,G1,F2. . .of the following forms:
∙ s=t,s<t,s>t,s≤t, ands≥t (comparisons)
∙ 1∣s,2∣s,3∣s, . . . (divisibility constraints)
∙ ⊤(true) and⊥(false) (propositional constants)
∙ F∨G(disjunction),F∧G(conjunction) and¬F(negation) (propositional connectives)
∙ ∃x.F(reads ”there exists anxsuch thatF”) and
∀x.F(reads ”for allx:F”) (first-order fragment) wheresandtare terms andxis a variable.
Furthermore, We allow brackets in formulas.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Notational conventions
∙ Relative precedence:¬(highest – binds tightest),∧,∨(lowest)
∙ The quantifiers∀xand∃xextend as far as possible to the right.
∙ ∀x1.∀x2. . . .∀xn.F is abbreviated to∀x1,x2, . . . ,xn.F
Example:
∀x.∃y.¬x+1=2y∧x>0∨y<2 means
∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Notational conventions
∙ Relative precedence:¬(highest – binds tightest),∧,∨(lowest)
∙ The quantifiers∀xand∃xextend as far as possible to the right.
∙ ∀x1.∀x2. . . .∀xn.F is abbreviated to∀x1,x2, . . . ,xn.F
Example:
∀x.∃y.¬x+1=2y∧x>0∨y<2 means
∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Notational conventions
∙ Relative precedence:¬(highest – binds tightest),∧,∨(lowest)
∙ The quantifiers∀xand∃xextend as far as possible to the right.
∙ ∀x1.∀x2. . . .∀xn.F is abbreviated to∀x1,x2, . . . ,xn.F
Example:
∀x.∃y.¬x+1=2y∧x>0∨y<2 means
∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Notational conventions
∙ Relative precedence:¬(highest – binds tightest),∧,∨(lowest)
∙ The quantifiers∀xand∃xextend as far as possible to the right.
∙ ∀x1.∀x2. . . .∀xn.F is abbreviated to∀x1,x2, . . . ,xn.F
Example:
∀x.∃y.¬x+1=2y∧x>0∨y<2 means
∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Notational conventions
∙ Relative precedence:¬(highest – binds tightest),∧,∨(lowest)
∙ The quantifiers∀xand∃xextend as far as possible to the right.
∙ ∀x1.∀x2. . . .∀xn.F is abbreviated to∀x1,x2, . . . ,xn.F
Example:
∀x.∃y.¬x+1=2y∧x>0∨y<2 means
∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Some concepts
∙ In∀x.F :
∙ xis called thequantified variable
∙ ∀xis called thequantifier
∙ Fis thescopeof the quantifier The case for∃x.F is similar.
∙ An occurrence of a variable x in a formula F is abound occurrenceif it occurs in the scope of a quantifier∀x or∃x in F.
Otherwise, that occurrence of x isfreein F .
∙ x is a free variable of F if there is some free occurrence of x in F .
∙ A formula is calledclosedif it contains no free variables;
otherwise it is called open.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Some concepts
∙ In∀x.F :
∙ xis called thequantified variable
∙ ∀xis called thequantifier
∙ Fis thescopeof the quantifier The case for∃x.F is similar.
∙ An occurrence of a variable x in a formula F is abound occurrenceif it occurs in the scope of a quantifier∀x or∃x in F.
Otherwise, that occurrence of x isfreein F .
∙ x is a free variable of F if there is some free occurrence of x in F .
∙ A formula is calledclosedif it contains no free variables;
otherwise it is called open.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Some concepts
∙ In∀x.F :
∙ xis called thequantified variable
∙ ∀xis called thequantifier
∙ Fis thescopeof the quantifier The case for∃x.F is similar.
∙ An occurrence of a variable x in a formula F is abound occurrenceif it occurs in the scope of a quantifier∀x or∃x in F.
Otherwise, that occurrence of x isfreein F .
∙ x is a free variable of F if there is some free occurrence of x in F .
∙ A formula is calledclosedif it contains no free variables;
otherwise it is called open.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Some concepts
∙ In∀x.F :
∙ xis called thequantified variable
∙ ∀xis called thequantifier
∙ Fis thescopeof the quantifier The case for∃x.F is similar.
∙ An occurrence of a variable x in a formula F is abound occurrenceif it occurs in the scope of a quantifier∀x or∃x in F.
Otherwise, that occurrence of x isfreein F .
∙ x is a free variable of F if there is some free occurrence of x in F .
∙ A formula is calledclosedif it contains no free variables;
otherwise it is called open.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Semantics
Letℤdenote the set of integers. . . ,−2,−1,0,1,2, . . ..
The operations+and−and the relations=, <,≤, >,≥have their standard meaning.
AinterpretationIassigns an integerI(x)∈ℤto every variablex.
LetI⊲{x7→v}be the x-variant ofIwhich is asIexcept thatvis assigned tox.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Semantics
Letℤdenote the set of integers. . . ,−2,−1,0,1,2, . . ..
The operations+and−and the relations=, <,≤, >,≥have their standard meaning.
AinterpretationIassigns an integerI(x)∈ℤto every variablex.
LetI⊲{x7→v}be the x-variant ofIwhich is asIexcept thatvis assigned tox.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Semantics
Letℤdenote the set of integers. . . ,−2,−1,0,1,2, . . ..
The operations+and−and the relations=, <,≤, >,≥have their standard meaning.
AinterpretationIassigns an integerI(x)∈ℤto every variablex.
LetI⊲{x7→v}be the x-variant ofIwhich is asIexcept thatvis assigned tox.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Semantics
Letℤdenote the set of integers. . . ,−2,−1,0,1,2, . . ..
The operations+and−and the relations=, <,≤, >,≥have their standard meaning.
AinterpretationIassigns an integerI(x)∈ℤto every variablex.
LetI⊲{x7→v}be the x-variant ofIwhich is asIexcept thatvis assigned tox.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Semantics of terms
Let an assignmentIbe given.
The semantics of a termsis an integerˆI(s)∈ℤdefined as follows:
ˆI(x) = I(x)
ˆI(a) = a where a∈ℤ
ˆI(s+t) = ˆI(s) + ˆI(t) ˆI(s−t) = ˆI(s)−ˆI(t)
ˆI(a⋅s) = a⋅ˆI(s) where a∈ℤ
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Semantics of formulas
Let an assignmentIbe given.
The semantic relationI∣=F is defined by structural induction on formulas:
I∣=s<t iff ˆI(s)<ˆI(t) other relations are similar I∣=a∣s iff a dividesˆI(s) where a∈ℤ
I∣=¬F iff not (I∣=F ) I∣=F∨G iff I∣=F or I∣=G I∣=F∧G iff I∣=F and I∣=G
I∣=∀x.F iff I⊲{x7→v} ∣=F for every v∈ℤ I∣=∃x.F iff I⊲{x7→v} ∣=F for some v∈ℤ
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Concepts
A formulaFissatisfiableif there is some assignmentIfor which the formula is true. Otherwise it isunsatisfiable.
A formula isvalidif it is true for all assignments.
Notice: The truth value of a closed formula is independent of the chosen assignment. It is either valid (true for all assignments), or unsatisfiable (false for all assignments).
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Concepts
A formulaFissatisfiableif there is some assignmentIfor which the formula is true. Otherwise it isunsatisfiable.
A formula isvalidif it is true for all assignments.
Notice: The truth value of a closed formula is independent of the chosen assignment. It is either valid (true for all assignments), or unsatisfiable (false for all assignments).
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Concepts
A formulaFissatisfiableif there is some assignmentIfor which the formula is true. Otherwise it isunsatisfiable.
A formula isvalidif it is true for all assignments.
Notice: The truth value of a closed formula is independent of the chosen assignment. It is either valid (true for all assignments), or unsatisfiable (false for all assignments).
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Examples
∙ ∃y.x=2y — (x is even) is satisfiable but not valid also expressible as 2∣x
∙ ∃y.x=2y∨x=2y+1— (x is even or x is odd) is valid also expressible as 2∣x∨2∣x+1
∙ ∃x.∀y.x≤yis unsatifiable (false)
∙ ∃x.∀y.x+y=yis valid (true)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Examples
∙ ∃y.x=2y — (x is even) is satisfiable but not valid also expressible as 2∣x
∙ ∃y.x=2y∨x=2y+1— (x is even or x is odd) is valid also expressible as 2∣x∨2∣x+1
∙ ∃x.∀y.x≤yis unsatifiable (false)
∙ ∃x.∀y.x+y=yis valid (true)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Examples
∙ ∃y.x=2y — (x is even) is satisfiable but not valid also expressible as 2∣x
∙ ∃y.x=2y∨x=2y+1— (x is even or x is odd) is valid also expressible as 2∣x∨2∣x+1
∙ ∃x.∀y.x≤yis unsatifiable (false)
∙ ∃x.∀y.x+y=yis valid (true)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Examples
∙ ∃y.x=2y — (x is even) is satisfiable but not valid also expressible as 2∣x
∙ ∃y.x=2y∨x=2y+1— (x is even or x is odd) is valid also expressible as 2∣x∨2∣x+1
∙ ∃x.∀y.x≤yis unsatifiable (false)
∙ ∃x.∀y.x+y=yis valid (true)
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier elimination
In the theory of real numbers an example ofquantifier eliminationis:
∃x.ax2+bx+c=0 is equivalent to b2−4ac≥0
where a,b,c∈ℝand a∕=0.
Presburger developed a method, which for an arbitrary Presburger formulaF gives to an equivalentquantifier-freeformulaG.
IfFis a closed formula, then the truth value ofGcan be computed.
For example, Cooper’s algorithm for Presburger Arithmetic transforms:
∃x.(3x+1<10∨7x−6>7)∧2∣x to the followingvariable- and quantifier-freeformula:
⋁42
j=1(42∣j∧21∣j)
∨
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier elimination
In the theory of real numbers an example ofquantifier eliminationis:
∃x.ax2+bx+c=0 is equivalent to b2−4ac≥0
where a,b,c∈ℝand a∕=0.
Presburger developed a method, which for an arbitrary Presburger formulaF gives to an equivalentquantifier-freeformulaG.
IfFis a closed formula, then the truth value ofGcan be computed.
For example, Cooper’s algorithm for Presburger Arithmetic transforms:
∃x.(3x+1<10∨7x−6>7)∧2∣x to the followingvariable- and quantifier-freeformula:
⋁42
j=1(42∣j∧21∣j)
∨
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier elimination
In the theory of real numbers an example ofquantifier eliminationis:
∃x.ax2+bx+c=0 is equivalent to b2−4ac≥0
where a,b,c∈ℝand a∕=0.
Presburger developed a method, which for an arbitrary Presburger formulaF gives to an equivalentquantifier-freeformulaG.
IfFis a closed formula, then the truth value ofGcan be computed.
For example, Cooper’s algorithm for Presburger Arithmetic transforms:
∃x.(3x+1<10∨7x−6>7)∧2∣x to the followingvariable- and quantifier-freeformula:
⋁42
j=1(42∣j∧21∣j)
∨
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier elimination
In the theory of real numbers an example ofquantifier eliminationis:
∃x.ax2+bx+c=0 is equivalent to b2−4ac≥0
where a,b,c∈ℝand a∕=0.
Presburger developed a method, which for an arbitrary Presburger formulaF gives to an equivalentquantifier-freeformulaG.
IfFis a closed formula, then the truth value ofGcan be computed.
For example, Cooper’s algorithm for Presburger Arithmetic transforms:
∃x.(3x+1<10∨7x−6>7)∧2∣x to the followingvariable- and quantifier-freeformula:
⋁42
j=1(42∣j∧21∣j)
∨
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier elimination
In the theory of real numbers an example ofquantifier eliminationis:
∃x.ax2+bx+c=0 is equivalent to b2−4ac≥0
where a,b,c∈ℝand a∕=0.
Presburger developed a method, which for an arbitrary Presburger formulaF gives to an equivalentquantifier-freeformulaG.
IfFis a closed formula, then the truth value ofGcan be computed.
For example, Cooper’s algorithm for Presburger Arithmetic transforms:
∃x.(3x+1<10∨7x−6>7)∧2∣x to the followingvariable- and quantifier-freeformula:
⋁42
j=1(42∣j∧21∣j)
∨
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier Elimination (II)
Excludingdivisible predicates a∣s from the Presburger Formulas quantifier elimination isnotpossible.
Lemma: IfF(y)is a quantifier-free formula with one free variabley.
Let
S={n∈ℤ∣F(n)is valid}
Then either
S∩ℤ+ or ℤ+∖S is finite
Consider the formula:∃x.2x=y.
∙ S∩ℤ+is the infinite set of positive even numbers
∙ ℤ+∖Sis the infinite set of positive odd numbers
The addition of divisibility predicates makes quantifier elimination possible for Presburger Arithmetic, and, e.g.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier Elimination (II)
Excludingdivisible predicates a∣s from the Presburger Formulas quantifier elimination isnotpossible.
Lemma: IfF(y)is a quantifier-free formula with one free variabley.
Let
S={n∈ℤ∣F(n)is valid}
Then either
S∩ℤ+ or ℤ+∖S is finite
Consider the formula:∃x.2x=y.
∙ S∩ℤ+is the infinite set of positive even numbers
∙ ℤ+∖Sis the infinite set of positive odd numbers
The addition of divisibility predicates makes quantifier elimination possible for Presburger Arithmetic, and, e.g.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier Elimination (II)
Excludingdivisible predicates a∣s from the Presburger Formulas quantifier elimination isnotpossible.
Lemma: IfF(y)is a quantifier-free formula with one free variabley.
Let
S={n∈ℤ∣F(n)is valid}
Then either
S∩ℤ+ or ℤ+∖S is finite
Consider the formula:∃x.2x=y.
∙ S∩ℤ+is the infinite set of positive even numbers
∙ ℤ+∖Sis the infinite set of positive odd numbers
The addition of divisibility predicates makes quantifier elimination possible for Presburger Arithmetic, and, e.g.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier Elimination (II)
Excludingdivisible predicates a∣s from the Presburger Formulas quantifier elimination isnotpossible.
Lemma: IfF(y)is a quantifier-free formula with one free variabley.
Let
S={n∈ℤ∣F(n)is valid}
Then either
S∩ℤ+ or ℤ+∖S is finite
Consider the formula:∃x.2x=y.
∙ S∩ℤ+is the infinite set of positive even numbers
∙ ℤ+∖Sis the infinite set of positive odd numbers
The addition of divisibility predicates makes quantifier elimination possible for Presburger Arithmetic, and, e.g.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier Elimination (II)
Excludingdivisible predicates a∣s from the Presburger Formulas quantifier elimination isnotpossible.
Lemma: IfF(y)is a quantifier-free formula with one free variabley.
Let
S={n∈ℤ∣F(n)is valid}
Then either
S∩ℤ+ or ℤ+∖S is finite
Consider the formula:∃x.2x=y.
∙ S∩ℤ+is the infinite set of positive even numbers
∙ ℤ+∖Sis the infinite set of positive odd numbers
The addition of divisibility predicates makes quantifier elimination possible for Presburger Arithmetic, and, e.g.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Quantifier Elimination (II)
Excludingdivisible predicates a∣s from the Presburger Formulas quantifier elimination isnotpossible.
Lemma: IfF(y)is a quantifier-free formula with one free variabley.
Let
S={n∈ℤ∣F(n)is valid}
Then either
S∩ℤ+ or ℤ+∖S is finite
Consider the formula:∃x.2x=y.
∙ S∩ℤ+is the infinite set of positive even numbers
∙ ℤ+∖Sis the infinite set of positive odd numbers
The addition of divisibility predicates makes quantifier elimination possible for Presburger Arithmetic, and, e.g.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Cooper’s procedure - main idea
Consider a formula∃x.F[x], whereF isquantifier free.
Main steps:
∙ PutF[x]on negation normal form, yieldingF1[x]
∙ NormalizeF1[x]to use<as the only comparison operator, yieldingF2[x]
∙ NormalizeF2[x]so that atomic formulas have one occurrence of x(at most), yieldingF3[x]
∙ NormalizeF3[x]so that the coefficients ofxis 1 (in atomic formulas containing x), yieldingF4[x′]
∙ Construct fromF4[x′]a quantifier-free formulaF5which is equivalent to∃x.F[x]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Cooper’s procedure - main idea
Consider a formula∃x.F[x], whereF isquantifier free.
Main steps:
∙ PutF[x]on negation normal form, yieldingF1[x]
∙ NormalizeF1[x]to use<as the only comparison operator, yieldingF2[x]
∙ NormalizeF2[x]so that atomic formulas have one occurrence of x(at most), yieldingF3[x]
∙ NormalizeF3[x]so that the coefficients ofxis 1 (in atomic formulas containing x), yieldingF4[x′]
∙ Construct fromF4[x′]a quantifier-free formulaF5which is equivalent to∃x.F[x]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Cooper’s procedure - main idea
Consider a formula∃x.F[x], whereF isquantifier free.
Main steps:
∙ PutF[x]on negation normal form, yieldingF1[x]
∙ NormalizeF1[x]to use<as the only comparison operator, yieldingF2[x]
∙ NormalizeF2[x]so that atomic formulas have one occurrence of x(at most), yieldingF3[x]
∙ NormalizeF3[x]so that the coefficients ofxis 1 (in atomic formulas containing x), yieldingF4[x′]
∙ Construct fromF4[x′]a quantifier-free formulaF5which is equivalent to∃x.F[x]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Cooper’s procedure - main idea
Consider a formula∃x.F[x], whereF isquantifier free.
Main steps:
∙ PutF[x]on negation normal form, yieldingF1[x]
∙ NormalizeF1[x]to use<as the only comparison operator, yieldingF2[x]
∙ NormalizeF2[x]so that atomic formulas have one occurrence of x(at most), yieldingF3[x]
∙ NormalizeF3[x]so that the coefficients ofxis 1 (in atomic formulas containing x), yieldingF4[x′]
∙ Construct fromF4[x′]a quantifier-free formulaF5which is equivalent to∃x.F[x]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Cooper’s procedure - main idea
Consider a formula∃x.F[x], whereF isquantifier free.
Main steps:
∙ PutF[x]on negation normal form, yieldingF1[x]
∙ NormalizeF1[x]to use<as the only comparison operator, yieldingF2[x]
∙ NormalizeF2[x]so that atomic formulas have one occurrence of x(at most), yieldingF3[x]
∙ NormalizeF3[x]so that the coefficients ofxis 1 (in atomic formulas containing x), yieldingF4[x′]
∙ Construct fromF4[x′]a quantifier-free formulaF5which is equivalent to∃x.F[x]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Negation Normal Form
Input: A quantifier-free formulaF[x].
Output: A formulaF1[x], where negation is used on literals only.
Technique: Apply de Morgan’s laws
¬(F∨G) ⇐⇒ ¬F∧ ¬G
¬(F∧G) ⇐⇒ ¬F∨ ¬G from left to right, together with:
¬¬F ⇐⇒ F
¬⊤ ⇐⇒ ⊥
¬⊥ ⇐⇒ ⊤
until no further application is possible.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Negation Normal Form
Input: A quantifier-free formulaF[x].
Output: A formulaF1[x], where negation is used on literals only.
Technique: Apply de Morgan’s laws
¬(F∨G) ⇐⇒ ¬F∧ ¬G
¬(F∧G) ⇐⇒ ¬F∨ ¬G from left to right, together with:
¬¬F ⇐⇒ F
¬⊤ ⇐⇒ ⊥
¬⊥ ⇐⇒ ⊤
until no further application is possible.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
2[x]
Output: A formulaF2[x]containing comparison<only, and where negation is applied to divisibility constraints only.
Technique: Use
s=t ⇐⇒ s<t+1∧t<s+1
¬(s=t) ⇐⇒ s<t∨t<s
¬(s<t) ⇐⇒ t<s+1
The other comparisons≤,≥, >can also be treated.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
3[x]
Output: A formulaF3[x], where atomic formulas contain one occurrence ofxat most.
Technique: Use linear arithmetic to bring each atomic formula containing x on the form
hx<t or t<hx or k∣hx+t
whereh,k∈ℤ+andxdoes not occur int.
Example:
6x+z<4x+3y−5 is transformed to
2x<3y−z−5
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
3[x]
Output: A formulaF3[x], where atomic formulas contain one occurrence ofxat most.
Technique: Use linear arithmetic to bring each atomic formula containing x on the form
hx<t or t<hx or k∣hx+t
whereh,k∈ℤ+andxdoes not occur int.
Example:
6x+z<4x+3y−5 is transformed to
2x<3y−z−5
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
4[x
′]
Output: A formulaF4[x′], where coefficients to x′are all 1 and
∃x.F[x] is equivalent to ∃x′.F[x′]
Let𝛿be the least common multiple (lcm) of all coefficients tox.
Normalize each constraint so that𝛿is the coefficient ofx. The resulting formula isF3′[𝛿x].F4[x′]isF3′[x′]∧𝛿∣x′
Example:
2x<z+6∧y−1<3x∧4∣5x+1
is transformed toF3′[30x]
30x<15z+90 ∧ 10y−10<30x ∧ 24∣30x+6 as30=lcm{2,3,5}, andF4[x′]is
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
4[x
′]
Output: A formulaF4[x′], where coefficients to x′are all 1 and
∃x.F[x] is equivalent to ∃x′.F[x′]
Let𝛿be the least common multiple (lcm) of all coefficients tox.
Normalize each constraint so that𝛿is the coefficient ofx. The resulting formula isF3′[𝛿x].F4[x′]isF3′[x′]∧𝛿∣x′
Example:
2x<z+6∧y−1<3x∧4∣5x+1
is transformed toF3′[30x]
30x<15z+90 ∧ 10y−10<30x ∧ 24∣30x+6 as30=lcm{2,3,5}, andF4[x′]is
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
4[x
′]
Output: A formulaF4[x′], where coefficients to x′are all 1 and
∃x.F[x] is equivalent to ∃x′.F[x′]
Let𝛿be the least common multiple (lcm) of all coefficients tox.
Normalize each constraint so that𝛿is the coefficient ofx. The resulting formula isF3′[𝛿x].F4[x′]isF3′[x′]∧𝛿∣x′
Example:
2x<z+6∧y−1<3x∧4∣5x+1
is transformed toF3′[30x]
30x<15z+90 ∧ 10y−10<30x ∧ 24∣30x+6 as30=lcm{2,3,5},andF4[x′]is
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
4[x
′]
Output: A formulaF4[x′], where coefficients to x′are all 1 and
∃x.F[x] is equivalent to ∃x′.F[x′]
Let𝛿be the least common multiple (lcm) of all coefficients tox.
Normalize each constraint so that𝛿is the coefficient ofx. The resulting formula isF3′[𝛿x].F4[x′]isF3′[x′]∧𝛿∣x′
Example:
2x<z+6∧y−1<3x∧4∣5x+1
is transformed toF3′[30x]
30x<15z+90 ∧ 10y−10<30x ∧ 24∣30x+6 as30=lcm{2,3,5}, andF4[x′]is
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
5– part 1
Output: Aquantifier-freeformulaF5which is equivalent to∃x.F[x]
(and to∃x′.F4[x′])
Each literal inF4[x′]containingx′has one of the forms:
(A)x′<a, (B)b<x′, (C)h∣x′+c, (D)¬(h∣x′+c) We distinguish two cases.
Case 1: there are infinitely many small satisfying assignments tox′. LetF−∞[x′]be obtained from F4[x′]by replacing:
∙ (A)-literals by⊤and
∙ (B)-literals by⊥.
Let
𝛿=lcm{h∣h∣x+c is a divisibility constraint in a (C) or (D) literal}.
LetF51be
⋁𝛿
F [j]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
5– part 1
Output: Aquantifier-freeformulaF5which is equivalent to∃x.F[x]
(and to∃x′.F4[x′])
Each literal inF4[x′]containingx′has one of the forms:
(A)x′<a, (B)b<x′, (C)h∣x′+c, (D)¬(h∣x′+c) We distinguish two cases.
Case 1: there are infinitely many small satisfying assignments tox′. LetF−∞[x′]be obtained from F4[x′]by replacing:
∙ (A)-literals by⊤and
∙ (B)-literals by⊥.
Let
𝛿=lcm{h∣h∣x+c is a divisibility constraint in a (C) or (D) literal}.
LetF51be
⋁𝛿
F [j]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
5– part 1
Output: Aquantifier-freeformulaF5which is equivalent to∃x.F[x]
(and to∃x′.F4[x′])
Each literal inF4[x′]containingx′has one of the forms:
(A)x′<a, (B)b<x′, (C)h∣x′+c, (D)¬(h∣x′+c) We distinguish two cases.
Case 1: there are infinitely many small satisfying assignments tox′. LetF−∞[x′]be obtained from F4[x′]by replacing:
∙ (A)-literals by⊤and
∙ (B)-literals by⊥.
Let
𝛿=lcm{h∣h∣x+c is a divisibility constraint in a (C) or (D) literal}.
LetF51be
⋁𝛿
F [j]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
5– part 1
Output: Aquantifier-freeformulaF5which is equivalent to∃x.F[x]
(and to∃x′.F4[x′])
Each literal inF4[x′]containingx′has one of the forms:
(A)x′<a, (B)b<x′, (C)h∣x′+c, (D)¬(h∣x′+c) We distinguish two cases.
Case 1: there are infinitely many small satisfying assignments tox′. LetF−∞[x′]be obtained from F4[x′]by replacing:
∙ (A)-literals by⊤and
∙ (B)-literals by⊥.
Let
𝛿=lcm{h∣h∣x+c is a divisibility constraint in a (C) or (D) literal}.
LetF51be
⋁𝛿
F [j]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
5– part 2
Each literal inF4[x′]containingx′has one of the forms:
(A)x′<a, (B)b<x′, (C)h∣x′+c, (D)¬(h∣x′+c) Case 2: there is a least satisfying assignments tox′.
For that assignment an (B) literal is true and for smaller assignments tox′the formula is false.
LetB={b∣b<x′is a (B) literal}
ThenF52is:
⋁𝛿 j=1
⋁
b∈B
F4[b+j]
ThenF5isF51∨F52i.e.
⋁𝛿
F−∞[j]∨
⋁𝛿 ⋁
F4[b+j]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
5– part 2
Each literal inF4[x′]containingx′has one of the forms:
(A)x′<a, (B)b<x′, (C)h∣x′+c, (D)¬(h∣x′+c) Case 2: there is a least satisfying assignments tox′.
For that assignment an (B) literal is true and for smaller assignments tox′the formula is false.
LetB={b∣b<x′is a (B) literal}
ThenF52is:
⋁𝛿 j=1
⋁
b∈B
F4[b+j]
ThenF5isF51∨F52i.e.
⋁𝛿
F−∞[j]∨
⋁𝛿 ⋁
F4[b+j]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Construction of F
5– part 2
Each literal inF4[x′]containingx′has one of the forms:
(A)x′<a, (B)b<x′, (C)h∣x′+c, (D)¬(h∣x′+c) Case 2: there is a least satisfying assignments tox′.
For that assignment an (B) literal is true and for smaller assignments tox′the formula is false.
LetB={b∣b<x′is a (B) literal}
ThenF52is:
⋁𝛿 j=1
⋁
b∈B
F4[b+j]
ThenF5isF51∨F52i.e.
⋁𝛿
F−∞[j]∨
⋁𝛿 ⋁
F4[b+j]
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Example (I)
∃x.(3x+1<10 ∨ 7x−6>7) ∧ 2∣x
| {z }
F[x]
F[x]is on Negation Normal Form. Isolate x and use<only:
∃x.(3x <9 ∨ 13<7x) ∧ 2∣x
| {z }
F3[x]
Normalize coefficient to x, part 1:
∃x.(21x<63 ∨ 39<21x) ∧ 42∣21x
| {z }
F3′[21x]
Normalize coefficient to x, part 2:
∃x′.(x′<63 ∨ 39<x′) ∧ 42∣x′ ∧ 21∣x′
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Example (I)
∃x.(3x+1<10 ∨ 7x−6>7) ∧ 2∣x
| {z }
F[x]
F[x]is on Negation Normal Form. Isolate x and use<only:
∃x.(3x <9 ∨ 13<7x) ∧ 2∣x
| {z }
F3[x]
Normalize coefficient to x, part 1:
∃x.(21x<63 ∨ 39<21x) ∧ 42∣21x
| {z }
F3′[21x]
Normalize coefficient to x, part 2:
∃x′.(x′<63 ∨ 39<x′) ∧ 42∣x′ ∧ 21∣x′
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Example (I)
∃x.(3x+1<10 ∨ 7x−6>7) ∧ 2∣x
| {z }
F[x]
F[x]is on Negation Normal Form. Isolate x and use<only:
∃x.(3x <9 ∨ 13<7x) ∧ 2∣x
| {z }
F3[x]
Normalize coefficient to x, part 1:
∃x.(21x<63 ∨ 39<21x) ∧ 42∣21x
| {z }
F3′[21x]
Normalize coefficient to x, part 2:
∃x′.(x′<63 ∨ 39<x′) ∧ 42∣x′ ∧ 21∣x′
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Example (I)
∃x.(3x+1<10 ∨ 7x−6>7) ∧ 2∣x
| {z }
F[x]
F[x]is on Negation Normal Form. Isolate x and use<only:
∃x.(3x <9 ∨ 13<7x) ∧ 2∣x
| {z }
F3[x]
Normalize coefficient to x, part 1:
∃x.(21x<63 ∨ 39<21x) ∧ 42∣21x
| {z }
F3′[21x]
Normalize coefficient to x, part 2:
∃x′.(x′<63 ∨ 39<x′) ∧ 42∣x′ ∧ 21∣x′
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Example (II)
∃x′.(x′<63 ∨ 39<x′) ∧ 42∣x′ ∧ 21∣x′
| {z }
F4[x′]
Eliminate the quantifier:
F−∞[x′] : (⊤ ∨ ⊥) ∧ 42∣x′ ∧21∣x′ 𝛿=lcm{21,42}=42
B={39}
⋁42
j=1(42∣j∧21∣j)
∨
⋁42
j=1((39+j<63∨39<39+j)∧42∣39+j∧21∣39+j) This formula istrueand so is
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Example (II)
∃x′.(x′<63 ∨ 39<x′) ∧ 42∣x′ ∧ 21∣x′
| {z }
F4[x′]
Eliminate the quantifier:
F−∞[x′] : (⊤ ∨ ⊥) ∧ 42∣x′ ∧21∣x′ 𝛿=lcm{21,42}=42
B={39}
⋁42
j=1(42∣j∧21∣j)
∨
⋁42
j=1((39+j<63∨39<39+j)∧42∣39+j∧21∣39+j) This formula istrueand so is
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Example (II)
∃x′.(x′<63 ∨ 39<x′) ∧ 42∣x′ ∧ 21∣x′
| {z }
F4[x′]
Eliminate the quantifier:
F−∞[x′] : (⊤ ∨ ⊥) ∧ 42∣x′ ∧21∣x′ 𝛿=lcm{21,42}=42
B={39}
⋁42
j=1(42∣j∧21∣j)
∨
⋁42
j=1((39+j<63∨39<39+j)∧42∣39+j∧21∣39+j) This formula istrueand so is
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Summary (I)
∙ Cooper’s algorithm can decide arbitrary formulas of Presbruger Arithmetic – even in the presence of arbitrary quantifications.
∙ The problem has a double exponential lower bound and a triple exponential upper bound.
∙ Cooper’s algorithm has a triple exponential upper bound.
∙ Many optimizations are possible.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Summary (I)
∙ Cooper’s algorithm can decide arbitrary formulas of Presbruger Arithmetic – even in the presence of arbitrary quantifications.
∙ The problem has a double exponential lower bound and a triple exponential upper bound.
∙ Cooper’s algorithm has a triple exponential upper bound.
∙ Many optimizations are possible.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Summary (I)
∙ Cooper’s algorithm can decide arbitrary formulas of Presbruger Arithmetic – even in the presence of arbitrary quantifications.
∙ The problem has a double exponential lower bound and a triple exponential upper bound.
∙ Cooper’s algorithm has a triple exponential upper bound.
∙ Many optimizations are possible.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Summary (I)
∙ Cooper’s algorithm can decide arbitrary formulas of Presbruger Arithmetic – even in the presence of arbitrary quantifications.
∙ The problem has a double exponential lower bound and a triple exponential upper bound.
∙ Cooper’s algorithm has a triple exponential upper bound.
∙ Many optimizations are possible.
02917 Ad- vanced
Top- ics in
Em- bed- ded Sys- tems
Michael R. Hansen
Summary (II)
The advantage with Cooper’s algorithm is that it does not require normal form, as some other decision methods do. Quantifier elimination in connection with DNF or CNF hurts a lot.
A disadvantage with Cooper’s algorithm is that constants obtained using lcm may be large.
Ongoing work: Experiments with a declarative implementation of the algorithm including many optimizations aiming at:
∙ including techniques from other decision methods, and
∙ a parallel implementation on a multi-core platform striving for a very efficient backend for DC-modelchecking.