• Ingen resultater fundet

02917AdvancedTopicsinEmbeddedSystems PresburgerArithmetic:Cooper’salgorithmMichaelR.Hansen 02917Ad-vancedTop-icsinEm-bed-dedSys-tems

N/A
N/A
Info
Hent
Protected

Academic year: 2022

Del "02917AdvancedTopicsinEmbeddedSystems PresburgerArithmetic:Cooper’salgorithmMichaelR.Hansen 02917Ad-vancedTop-icsinEm-bed-dedSys-tems"

Copied!
84
0
0

Indlæser.... (se fuldtekst nu)

Hele teksten

(1)

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

(2)

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.

(3)

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.

(4)

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.

(5)

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.

(6)

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

(7)

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

(8)

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

(9)

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

(10)

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,st, andst (comparisons)

1∣s,2∣s,3∣s, . . . (divisibility constraints)

⊤(true) and⊥(false) (propositional constants)

FG(disjunction),FG(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.

(11)

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,st, andst (comparisons)

1∣s,2∣s,3∣s, . . . (divisibility constraints)

⊤(true) and⊥(false) (propositional constants)

FG(disjunction),FG(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.

(12)

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,st, andst (comparisons)

1∣s,2∣s,3∣s, . . . (divisibility constraints)

⊤(true) and⊥(false) (propositional constants)

FG(disjunction),FG(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.

(13)

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,st, andst (comparisons)

1∣s,2∣s,3∣s, . . . (divisibility constraints)

⊤(true) and⊥(false) (propositional constants)

FG(disjunction),FG(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.

(14)

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,st, andst (comparisons)

1∣s,2∣s,3∣s, . . . (divisibility constraints)

⊤(true) and⊥(false) (propositional constants)

FG(disjunction),FG(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.

(15)

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,st, andst (comparisons)

1∣s,2∣s,3∣s, . . . (divisibility constraints)

⊤(true) and⊥(false) (propositional constants)

FG(disjunction),FG(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.

(16)

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,st, andst (comparisons)

1∣s,2∣s,3∣s, . . . (divisibility constraints)

⊤(true) and⊥(false) (propositional constants)

FG(disjunction),FG(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.

(17)

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=2yx>0∨y<2 means

∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)

(18)

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=2yx>0∨y<2 means

∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)

(19)

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=2yx>0∨y<2 means

∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)

(20)

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=2yx>0∨y<2 means

∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)

(21)

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=2yx>0∨y<2 means

∀x.∃y.(((¬x+1=2y)∧x>0)∨y<2)

(22)

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.

(23)

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.

(24)

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.

(25)

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.

(26)

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.

(27)

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.

(28)

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.

(29)

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.

(30)

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(st) = ˆI(s)−ˆI(t)

ˆI(as) = a⋅ˆI(s) where a∈ℤ

(31)

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∣=FG iff I∣=F or I∣=G I∣=FG 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∈ℤ

(32)

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

(33)

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

(34)

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

(35)

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=2yx=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)

(36)

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=2yx=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)

(37)

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=2yx=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)

(38)

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=2yx=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)

(39)

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 b24ac≥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)

(40)

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 b24ac≥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)

(41)

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 b24ac≥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)

(42)

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 b24ac≥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)

(43)

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 b24ac≥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)

(44)

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.

(45)

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.

(46)

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.

(47)

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.

(48)

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.

(49)

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.

(50)

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]

(51)

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]

(52)

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]

(53)

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]

(54)

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]

(55)

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.

(56)

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.

(57)

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<tt<s

¬(s<t) ⇐⇒ t<s+1

The other comparisons≤,≥, >can also be treated.

(58)

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<3yz−5

(59)

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<3yz−5

(60)

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 xare 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

(61)

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 xare 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

(62)

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 xare 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

(63)

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 xare 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

(64)

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]containingxhas 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]

(65)

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]containingxhas 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]

(66)

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]containingxhas 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]

(67)

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]containingxhas 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]

(68)

02917 Ad- vanced

Top- ics in

Em- bed- ded Sys- tems

Michael R. Hansen

Construction of F

5

– part 2

Each literal inF4[x]containingxhas 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 toxthe formula is false.

LetB={b∣b<xis a (B) literal}

ThenF52is:

𝛿 j=1

b∈B

F4[b+j]

ThenF5isF51F52i.e.

𝛿

F−∞[j]∨

𝛿

F4[b+j]

(69)

02917 Ad- vanced

Top- ics in

Em- bed- ded Sys- tems

Michael R. Hansen

Construction of F

5

– part 2

Each literal inF4[x]containingxhas 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 toxthe formula is false.

LetB={b∣b<xis a (B) literal}

ThenF52is:

𝛿 j=1

b∈B

F4[b+j]

ThenF5isF51F52i.e.

𝛿

F−∞[j]∨

𝛿

F4[b+j]

(70)

02917 Ad- vanced

Top- ics in

Em- bed- ded Sys- tems

Michael R. Hansen

Construction of F

5

– part 2

Each literal inF4[x]containingxhas 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 toxthe formula is false.

LetB={b∣b<xis a (B) literal}

ThenF52is:

𝛿 j=1

b∈B

F4[b+j]

ThenF5isF51F52i.e.

𝛿

F−∞[j]∨

𝛿

F4[b+j]

(71)

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

(72)

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

(73)

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

(74)

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

(75)

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

(76)

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

(77)

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

(78)

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.

(79)

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.

(80)

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.

(81)

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.

(82)

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.

Referencer

RELATEREDE DOKUMENTER

It has been done for arbitrary nilpotent groups of class ≤ 3 and in the case of symmetric 2-words also for dihedral group of order 2 p.. In the papers [2] and [9] 2-words are

Our method is to combine an elementary bound on the size of the relevant space of free products with some number theory to give a finite number of can- didates for arithmetic

During the 1970s, Danish mass media recurrently portrayed mass housing estates as signifiers of social problems in the otherwise increasingl affluent anish

The Healthy Home project explored how technology may increase collaboration between patients in their homes and the network of healthcare professionals at a hospital, and

Most specific to our sample, in 2006, there were about 40% of long-term individuals who after the termination of the subsidised contract in small firms were employed on

Freedom in commons brings ruin to all.” In terms of National Parks – an example with much in common with museums – Hardin diagnoses that being ‘open to all, without limits’

THEOREM 2: For arbitrary t ≥ 0 , algorithm SM(n,t) solves BG problem for at most t illoyal generals... PROOF of

Based on this, each study was assigned an overall weight of evidence classification of “high,” “medium” or “low.” The overall weight of evidence may be characterised as