02917 Advanced Topics in Embedded Systems

(1)

02917 Advanced

Topics in Embedded

Systems Michael R. Hansen

02917 Advanced Topics in Embedded Systems

Model Checking for Duration Calculus using Presburger Arithmetic

Michael R. Hansen

(2)

02917 Advanced

Topics in Embedded

Overview

∙ Overview of fundamental (un)decidability results

∙ A basic decidability results – with non-elementary complexity

∙ Towards efficient model checking based on approximations Using Presburger Arithmetic: first-order logic of natural numbers with addition

∙ Decision procedure for Presburger Arithmetic

(3)

02917 Advanced

Topics in Embedded

Overview

∙ Overview of fundamental (un)decidability results

∙ A basic decidability results – with non-elementary complexity

∙ Towards efficient model checking based on approximations Using Presburger Arithmetic: first-order logic of natural numbers with addition

∙ Decision procedure for Presburger Arithmetic

(4)

02917 Advanced

Topics in Embedded

Overview

∙ Overview of fundamental (un)decidability results

∙ A basic decidability results – with non-elementary complexity

∙ Towards efficient model checking based on approximations Using Presburger Arithmetic: first-order logic of natural numbers with addition

∙ Decision procedure for Presburger Arithmetic

(5)

02917 Advanced

Topics in Embedded

Overview

∙ Overview of fundamental (un)decidability results

∙ A basic decidability results – with non-elementary complexity

∙ Towards efficient model checking based on approximations Using Presburger Arithmetic: first-order logic of natural numbers with addition

∙ Decision procedure for Presburger Arithmetic

(6)

02917 Advanced

Topics in Embedded

Overview

∙ Overview of fundamental (un)decidability results

∙ A basic decidability results – with non-elementary complexity

∙ Towards efficient model checking based on approximations Using Presburger Arithmetic: first-order logic of natural numbers with addition

∙ Decision procedure for Presburger Arithmetic

(7)

02917 Advanced

Topics in Embedded

Basic Decidability Properties of Duration Calculus

Zhou Hansen Sestoft 93 Restricted Duration Calculus:

∙ ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

Satisfiability is reduced to emptiness of regular languages Decidable result for both discrete and continuous time Seemingly small extensions give undecidable subsets

RDC

1

(Cont. time) RDC

2

RDC

3

∙ ℓ = r , ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ∫ S

1

= ∫

S

2

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ℓ = x, ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ (∃x)𝜙

(8)

02917 Advanced

Topics in Embedded

Basic Decidability Properties of Duration Calculus

Zhou Hansen Sestoft 93 Restricted Duration Calculus:

∙ ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

Satisfiability is reduced to emptiness of regular languages Decidable result for both discrete and continuous time Seemingly small extensions give undecidable subsets

RDC

1

(Cont. time) RDC

2

RDC

3

∙ ℓ = r , ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ∫ S

1

= ∫

S

2

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ℓ = x, ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ (∃x)𝜙

(9)

02917 Advanced

Topics in Embedded

Basic Decidability Properties of Duration Calculus

Zhou Hansen Sestoft 93 Restricted Duration Calculus:

∙ ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

Satisfiability is reduced to emptiness of regular languages Decidable result for both discrete and continuous time Seemingly small extensions give undecidable subsets

RDC

1

(Cont. time) RDC

2

RDC

3

∙ ℓ = r , ⌈⌈ S ⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ∫ S

1

= ∫

S

2

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ℓ = x, ⌈⌈ S ⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ (∃ x)𝜙

(10)

02917 Advanced

Topics in Embedded

Basic Decidability Properties of Duration Calculus

Zhou Hansen Sestoft 93 Restricted Duration Calculus:

∙ ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

Satisfiability is reduced to emptiness of regular languages Decidable result for both discrete and continuous time Seemingly small extensions give undecidable subsets

RDC

1

(Cont. time) RDC

2

RDC

3

∙ ℓ = r , ⌈⌈ S ⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ∫ S

1

= ∫

S

2

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ℓ = x, ⌈⌈ S ⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ (∃ x)𝜙

(11)

02917 Advanced

Topics in Embedded

Basic Decidability Properties of Duration Calculus

Zhou Hansen Sestoft 93 Restricted Duration Calculus:

∙ ⌈⌈S⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

Satisfiability is reduced to emptiness of regular languages Decidable result for both discrete and continuous time Seemingly small extensions give undecidable subsets

RDC

1

(Cont. time) RDC

2

RDC

3

∙ ℓ = r , ⌈⌈ S ⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ∫ S

1

= ∫

S

2

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ ℓ = x, ⌈⌈ S ⌉⌉

∙ ¬𝜙, 𝜙 ∨ 𝜓, 𝜙

^⌢

𝜓

∙ (∃ x)𝜙

(12)

02917 Advanced

Topics in Embedded

Decidability of RDC for Discrete Time

Satisfiability is reduced to emptiness of regular languages

Idea: a ∈ Σ describes a piece of an interpretation, e.g. P

1

∧ ¬P

2

∧ P

3

Discrete time — one letter corresponds to one time unit.

ℒ(⌈⌈ S ⌉⌉) = (DNF (S))

⁺

ℒ(𝜑 ∨ 𝜓) = ℒ(𝜑) ∪ ℒ(𝜓) ℒ(¬𝜑) = Σ

^∗

∖ ℒ(𝜑) ℒ(𝜑

^⌢

𝜓) = ℒ(𝜑) ℒ(𝜓)

∙ ℒ(𝜙) is regular

∙ 𝜙 is satisfiable iff ℒ(𝜙) ∕= ∅

∙ Satisfiability problem for RDC is decidable

non-elementary complexity

(13)

02917 Advanced

Topics in Embedded

Decidability of RDC for Discrete Time

Satisfiability is reduced to emptiness of regular languages

Idea: a ∈ Σ describes a piece of an interpretation, e.g. P

1

∧ ¬P

2

∧ P

3

Discrete time — one letter corresponds to one time unit.

ℒ(⌈⌈ S ⌉⌉) = (DNF (S))

⁺

ℒ(𝜑 ∨ 𝜓) = ℒ(𝜑) ∪ ℒ(𝜓) ℒ(¬𝜑) = Σ

^∗

∖ ℒ(𝜑) ℒ(𝜑

^⌢

𝜓) = ℒ(𝜑) ℒ(𝜓)

∙ ℒ(𝜙) is regular

∙ 𝜙 is satisfiable iff ℒ(𝜙) ∕= ∅

∙ Satisfiability problem for RDC is decidable

non-elementary complexity

(14)

02917 Advanced

Topics in Embedded

Decidability of RDC for Discrete Time

Satisfiability is reduced to emptiness of regular languages

Idea: a ∈ Σ describes a piece of an interpretation, e.g. P

1

∧ ¬P

2

∧ P

3

Discrete time — one letter corresponds to one time unit.

ℒ(⌈⌈ S ⌉⌉) = (DNF (S))

⁺

ℒ(𝜑 ∨ 𝜓) = ℒ(𝜑) ∪ ℒ(𝜓) ℒ(¬𝜑) = Σ

^∗

∖ ℒ(𝜑) ℒ(𝜑

^⌢

𝜓) = ℒ(𝜑) ℒ(𝜓)

∙ ℒ(𝜙) is regular

∙ 𝜙 is satisfiable iff ℒ(𝜙) ∕= ∅

∙ Satisfiability problem for RDC is decidable

non-elementary complexity

(15)

02917 Advanced

Topics in Embedded

Decidability of RDC for Discrete Time

Satisfiability is reduced to emptiness of regular languages

Idea: a ∈ Σ describes a piece of an interpretation, e.g. P

1

∧ ¬P

2

∧ P

3

Discrete time — one letter corresponds to one time unit.

ℒ(⌈⌈ S ⌉⌉) = (DNF (S))

⁺

ℒ(𝜑 ∨ 𝜓) = ℒ(𝜑) ∪ ℒ(𝜓) ℒ(¬𝜑) = Σ

^∗

∖ ℒ(𝜑) ℒ(𝜑

^⌢

𝜓) = ℒ(𝜑) ℒ(𝜓)

∙ ℒ(𝜙) is regular

∙ 𝜙 is satisfiable iff ℒ(𝜙) ∕= ∅

∙ Satisfiability problem for RDC is decidable

non-elementary complexity

(16)

02917 Advanced

Topics in Embedded

Decidability of RDC for Discrete Time

Satisfiability is reduced to emptiness of regular languages

Idea: a ∈ Σ describes a piece of an interpretation, e.g. P

1

∧ ¬P

2

∧ P

3

Discrete time — one letter corresponds to one time unit.

ℒ(⌈⌈ S ⌉⌉) = (DNF (S))

⁺

ℒ(𝜑 ∨ 𝜓) = ℒ(𝜑) ∪ ℒ(𝜓) ℒ(¬𝜑) = Σ

^∗

∖ ℒ(𝜑) ℒ(𝜑

^⌢

𝜓) = ℒ(𝜑) ℒ(𝜓)

∙ ℒ(𝜙) is regular

∙ 𝜙 is satisfiable iff ℒ(𝜙) ∕= ∅

∙ Satisfiability problem for RDC is decidable

non-elementary complexity

(17)

02917 Advanced

Topics in Embedded

Status

∙ A DC fragment based on (propositional logic and chop) with almost no notion of duration has non-elementary complexity.

No existing tool is used on a daily basis.

∙ Fragments (propositional logic and chop) having simple notions of duration are undecidable.

So what about tool support?

(18)

02917 Advanced

Topics in Embedded

Status

∙ A DC fragment based on (propositional logic and chop) with almost no notion of duration has non-elementary complexity.

No existing tool is used on a daily basis.

∙ Fragments (propositional logic and chop) having simple notions of duration are undecidable.

So what about tool support?

(19)

02917 Advanced

Topics in Embedded

Status

∙ A DC fragment based on (propositional logic and chop) with almost no notion of duration has non-elementary complexity.

No existing tool is used on a daily basis.

∙ Fragments (propositional logic and chop) having simple notions of duration are undecidable.

So what about tool support?

(20)

02917 Advanced

Topics in Embedded

An example

Given Kripke structure K and a (certain kind of) DC formula 𝜙.

∙ Does K ∣ = 𝜙 hold? every trace t r satisfies 𝜙 non-elementary

Example: A simple Kripke structure K :

¬ p 1

p 3

2 4

¬ p p

Problem: K ∣ = □ (ℓ < 4 ⇒ ∫

p < 3)? YES

∙ Example run:

tr = (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (3 : ) satisfies □(ℓ < 4 ⇒ ∫

p < 3)

Branching-time approximations for efficient verification

Fr ¨anzleHansen 08,09

(21)

02917 Advanced

Topics in Embedded

An example

Given Kripke structure K and a (certain kind of) DC formula 𝜙.

∙ Does K ∣ = 𝜙 hold? every trace t r satisfies 𝜙 non-elementary

Example: A simple Kripke structure K :

¬ p 1

p 3

2 4

¬ p p

Problem: K ∣ = □ (ℓ < 4 ⇒ ∫

p < 3)? YES

∙ Example run:

tr = (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (3 : ) satisfies □(ℓ < 4 ⇒ ∫

p < 3)

Branching-time approximations for efficient verification

(22)

02917 Advanced

Topics in Embedded

An example

Given Kripke structure K and a (certain kind of) DC formula 𝜙.

∙ Does K ∣ = 𝜙 hold? every trace t r satisfies 𝜙 non-elementary

Example: A simple Kripke structure K :

¬ p 1

p 3

2 4

¬ p p

Problem: K ∣ = □ (ℓ < 4 ⇒ ∫

p < 3)? YES

∙ Example run:

tr = (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (3 : ) satisfies □(ℓ < 4 ⇒ ∫

p < 3)

Branching-time approximations for efficient verification

Fr ¨anzleHansen 08,09

(23)

02917 Advanced

Topics in Embedded

An example

Given Kripke structure K and a (certain kind of) DC formula 𝜙.

∙ Does K ∣ = 𝜙 hold? every trace t r satisfies 𝜙 non-elementary

Example: A simple Kripke structure K :

¬ p 1

p 3

2 4

¬ p p

Problem: K ∣ = □ (ℓ < 4 ⇒ ∫

p < 3)? YES

∙ Example run:

tr = (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (1 : ¬ p) (2 : p) (3 : ) satisfies □(ℓ < 4 ⇒ ∫

p < 3)

Branching-time approximations for efficient verification

(24)

02917 Advanced

Topics in Embedded

Branching-time approximations: Counting semantics

Ideas:

∙ All traces between two vertices are treated uniformly

∙ Add information on the frequency of visits to vertices.

m : Mset = V −→

^part

ℕ a multiset

The counting semantics: K [[𝜙]]

c

: V → V → Mset → 2

^𝔹

:

∙ K [[𝜙]]

c

i j m = {true} when t r ∣ =

K

𝜙, for any run t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {false} when t r ∕∣ =

K

𝜙, for any t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {true, false} if K is not consistent with m, i, j

∙ K [[𝜙]]

c

i j m = ∅ otherwise.

(25)

02917 Advanced

Topics in Embedded

Branching-time approximations: Counting semantics

Ideas:

∙ All traces between two vertices are treated uniformly

∙ Add information on the frequency of visits to vertices.

m : Mset = V −→

^part

ℕ a multiset

The counting semantics: K [[𝜙]]

c

: V → V → Mset → 2

^𝔹

:

∙ K [[𝜙]]

c

i j m = {true} when t r ∣ =

K

𝜙, for any run t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {false} when t r ∕∣ =

K

𝜙, for any t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {true, false} if K is not consistent with m, i, j

∙ K [[𝜙]]

c

i j m = ∅ otherwise.

(26)

02917 Advanced

Topics in Embedded

Branching-time approximations: Counting semantics

Ideas:

∙ All traces between two vertices are treated uniformly

∙ Add information on the frequency of visits to vertices.

m : Mset = V −→

^part

ℕ a multiset

The counting semantics: K [[𝜙]]

c

: V → V → Mset → 2

^𝔹

:

∙ K [[𝜙]]

c

i j m = {true} when t r ∣ =

K

𝜙, for any run t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {false} when t r ∕∣ =

K

𝜙, for any t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {true, false} if K is not consistent with m, i, j

∙ K [[𝜙]]

c

i j m = ∅ otherwise.

(27)

02917 Advanced

Topics in Embedded

Branching-time approximations: Counting semantics

Ideas:

∙ All traces between two vertices are treated uniformly

∙ Add information on the frequency of visits to vertices.

m : Mset = V −→

^part

ℕ a multiset

The counting semantics: K [[𝜙]]

c

: V → V → Mset → 2

^𝔹

:

∙ K [[𝜙]]

c

i j m = {true} when t r ∣ =

K

𝜙, for any run t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {false} when t r ∕∣ =

K

𝜙, for any t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {true, false} if K is not consistent with m, i, j

∙ K [[𝜙]]

c

i j m = ∅ otherwise.

(28)

02917 Advanced

Topics in Embedded

Branching-time approximations: Counting semantics

Ideas:

∙ All traces between two vertices are treated uniformly

∙ Add information on the frequency of visits to vertices.

m : Mset = V −→

^part

ℕ a multiset

The counting semantics: K [[𝜙]]

c

: V → V → Mset → 2

^𝔹

:

∙ K [[𝜙]]

c

i j m = {true} when t r ∣ =

K

𝜙, for any run t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {false} when t r ∕∣ =

K

𝜙, for any t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {true, false} if K is not consistent with m, i, j

∙ K [[𝜙]]

c

i j m = ∅ otherwise.

(29)

02917 Advanced

Topics in Embedded

Branching-time approximations: Counting semantics

Ideas:

∙ All traces between two vertices are treated uniformly

∙ Add information on the frequency of visits to vertices.

m : Mset = V −→

^part

ℕ a multiset

The counting semantics: K [[𝜙]]

c

: V → V → Mset → 2

^𝔹

:

∙ K [[𝜙]]

c

i j m = {true} when t r ∣ =

K

𝜙, for any run t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {false} when t r ∕∣ =

K

𝜙, for any t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {true, false} if K is not consistent with m, i, j

∙ K [[𝜙]]

c

i j m = ∅ otherwise.

(30)

02917 Advanced

Topics in Embedded

Branching-time approximations: Counting semantics

Ideas:

∙ All traces between two vertices are treated uniformly

∙ Add information on the frequency of visits to vertices.

m : Mset = V −→

^part

ℕ a multiset

The counting semantics: K [[𝜙]]

c

: V → V → Mset → 2

^𝔹

:

∙ K [[𝜙]]

c

i j m = {true} when t r ∣ =

K

𝜙, for any run t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {false} when t r ∕∣ =

K

𝜙, for any t r from i to j which is consistent with m

∙ K [[𝜙]]

c

i j m = {true, false} if K is not consistent with m, i, j

∙ K [[𝜙]]

c

i j m = ∅ otherwise.

(31)

02917 Advanced

Topics in Embedded

Model checking: Main idea

Given K , 𝜙 and a vector m = dom m of variables.

We mark situation pairs (i, j), with (𝜓, b, lin(m)), b ∈ {true, false}, where 𝜓 is a subformula of 𝜙

∙ and lin(m) is a side-condition (Presburger formula) with m as free variables.

Key properties for marking (𝜓, true, lin(m)):

∙

true ∈ K [[𝜓]] i j m for any m satisfying lin(m)

There are similar properties for a marking (𝜓, false, lin(m))

(32)

02917 Advanced

Topics in Embedded

Model checking: Main idea

Given K , 𝜙 and a vector m = dom m of variables.

We mark situation pairs (i, j), with (𝜓, b, lin(m)), b ∈ {true, false}, where 𝜓 is a subformula of 𝜙

∙ and lin(m) is a side-condition (Presburger formula) with m as free variables.

Key properties for marking (𝜓, true, lin(m)):

∙

true ∈ K [[𝜓]] i j m for any m satisfying lin(m)

There are similar properties for a marking (𝜓, false, lin(m))

(33)

02917 Advanced

Topics in Embedded

Model checking: Main idea

Given K , 𝜙 and a vector m = dom m of variables.

We mark situation pairs (i, j), with (𝜓, b, lin(m)), b ∈ {true, false}, where 𝜓 is a subformula of 𝜙

∙ and lin(m) is a side-condition (Presburger formula) with m as free variables.

Key properties for marking (𝜓, true, lin(m)):

∙

true ∈ K [[𝜓]] i j m for any m satisfying lin(m)

There are similar properties for a marking (𝜓, false, lin(m))

(34)

02917 Advanced

Topics in Embedded

Model checking: Main idea

Given K , 𝜙 and a vector m = dom m of variables.

We mark situation pairs (i, j), with (𝜓, b, lin(m)), b ∈ {true, false}, where 𝜓 is a subformula of 𝜙

∙ and lin(m) is a side-condition (Presburger formula) with m as free variables.

Key properties for marking (𝜓, true, lin(m)):

∙

true ∈ K [[𝜓]] i j m for any m satisfying lin(m)

There are similar properties for a marking (𝜓, false, lin(m))

(35)

02917 Advanced

Topics in Embedded

A Condition for Consistency

C(K , i

0

, j

0

, m) is a system of linear equations:

m-consistency wrt. K , i

0

and j

0

is equivalent to satisfiability of C(K , i

0

, j

0

, m) Variables:

∙ x

i

for every i ∈ V,

∙ x

ij

for every edge (i, j) ∈ E

∙ m[k] for every k ∈ dom m Main ideas:

∙ The ”inflow” is the same as the ”outflow” for any vertex k.

∙ i

0

has an extra inflow of 1 and j

0

has an extra outflow of 1.

∙ x

k

= m[k] for every k ∈ dom m.

For example, for every k ∈ V ∖ {i

0

, j

0

}:

Σ

(l,k)∈E

x

lk

= x

k

and x

k

= Σ

(k,l)∈E

x

kl

(36)

02917 Advanced

Topics in Embedded

A Condition for Consistency

C(K , i

0

, j

0

, m) is a system of linear equations:

m-consistency wrt. K , i

0

and j

0

is equivalent to satisfiability of C(K , i

0

, j

0

, m) Variables:

∙ x

i

for every i ∈ V,

∙ x

ij

for every edge (i, j) ∈ E

∙ m[k] for every k ∈ dom m Main ideas:

∙ The ”inflow” is the same as the ”outflow” for any vertex k.

∙ i

0

has an extra inflow of 1 and j

0

has an extra outflow of 1.

∙ x

k

= m[k] for every k ∈ dom m.

For example, for every k ∈ V ∖ {i

0

, j

0

}:

Σ

(l,k)∈E

x

lk

= x

k

and x

k

= Σ

(k,l)∈E

x

kl

(37)

02917 Advanced

Topics in Embedded

A Condition for Consistency

C(K , i

0

, j

0

, m) is a system of linear equations:

m-consistency wrt. K , i

0

and j

0

is equivalent to satisfiability of C(K , i

0

, j

0

, m) Variables:

∙ x

i

for every i ∈ V,

∙ x

ij

for every edge (i, j) ∈ E

∙ m[k] for every k ∈ dom m Main ideas:

∙ The ”inflow” is the same as the ”outflow” for any vertex k.

∙ i

0

has an extra inflow of 1 and j

0

has an extra outflow of 1.

∙ x

k

= m[k] for every k ∈ dom m.

For example, for every k ∈ V ∖ {i

0

, j

0

}:

Σ

(l,k)∈E

x

lk

= x

k

and x

k

= Σ

(k,l)∈E

x

kl

(38)

02917 Advanced

Topics in Embedded

A Condition for Consistency

C(K , i

0

, j

0

, m) is a system of linear equations:

m-consistency wrt. K , i

0

and j

0

is equivalent to satisfiability of C(K , i

0

, j

0

, m) Variables:

∙ x

i

for every i ∈ V,

∙ x

ij

for every edge (i, j) ∈ E

∙ m[k] for every k ∈ dom m Main ideas:

∙ The ”inflow” is the same as the ”outflow” for any vertex k.

∙ i

0

has an extra inflow of 1 and j

0

has an extra outflow of 1.

∙ x

k

= m[k] for every k ∈ dom m.

For example, for every k ∈ V ∖ {i

0

, j

0

}:

Σ

(l,k)∈E

x

lk

= x

k

and x

k

= Σ

(k,l)∈E

x

kl

(39)

02917 Advanced

Topics in Embedded

Model checking: Case 𝜓 = ∫ S < k

Markings for (i , j):

∙ (

∫ S < k, true, (

C(K , i, j, m, e) ∧ ∑

v∈domm,v∣=S

m[v] < k ))

∙ ( ∫

S < k, false, (

C(K , i, j, m, e) ∧ ∑

v∈domm,v∣=S

m[v] ≥ k ))

This is easily generalized to formulas of the form:

Σ

ⁿi=1

c

i

∫ S

i

⊲ k

where ⊲ ∈ {<, ≤, =, ≥, >} .

(40)

02917 Advanced

Topics in Embedded

Model checking: Case 𝜓 = ∫ S < k

Markings for (i , j):

∙ (

∫ S < k, true, (

C(K , i, j, m, e) ∧ ∑

v∈domm,v∣=S

m[v] < k ))

∙ ( ∫

S < k, false, (

C(K , i, j, m, e) ∧ ∑

v∈domm,v∣=S

m[v] ≥ k ))

This is easily generalized to formulas of the form:

Σ

ⁿi=1

c

i

∫ S

i

⊲ k

where ⊲ ∈ {<, ≤, =, ≥, >} .

(41)

02917 Advanced

Topics in Embedded

Model checking: Case 𝜓 = ∫ S < k

Markings for (i , j):

∙ (

∫ S < k, true, (

C(K , i, j, m, e) ∧ ∑

v∈domm,v∣=S

m[v] < k ))

∙ ( ∫

S < k, false, (

C(K , i, j, m, e) ∧ ∑

v∈domm,v∣=S

m[v] ≥ k ))

This is easily generalized to formulas of the form:

Σ

ⁿi=1

c

i

∫ S

i

⊲ k

where ⊲ ∈ {<, ≤, =, ≥, >} .

(42)

02917 Advanced

Topics in Embedded

Model checking: Case 𝜙 = 𝜓 ₁ ∧ 𝜓 ₂

Markings for (i , j):

∙ The true marking is (𝜓

1

∧ 𝜓

2

, true, 𝜇 ∧ 𝜈) iff (i, j) is marked with (𝜓

1

, true, 𝜇) and (𝜓

2

, true, 𝜈)

∙ The false marking is (𝜓

1

∧ 𝜓

2

, false, 𝜇 ∨ 𝜈) iff (i, j) is marked

with (𝜓

1

, false, 𝜇) and (𝜓

2

, false, 𝜈)

(43)

02917 Advanced

Topics in Embedded

Model checking: Case 𝜙 = 𝜓 ₁ ∧ 𝜓 ₂

Markings for (i , j):

∙ The true marking is (𝜓

1

∧ 𝜓

2

, true, 𝜇 ∧ 𝜈) iff (i, j) is marked with (𝜓

1

, true, 𝜇) and (𝜓

2

, true, 𝜈)

∙ The false marking is (𝜓

1

∧ 𝜓

2

, false, 𝜇 ∨ 𝜈) iff (i, j) is marked

with (𝜓

1

, false, 𝜇) and (𝜓

2

, false, 𝜈)

(44)

02917 Advanced

Topics in Embedded

Model checking: Case 𝜙 = ¬ 𝜓

Markings for (i , j):

∙ The true marking is (¬𝜓, true, 𝜇) iff (i, j) is marked with (𝜓, false, 𝜇)

∙ The false marking is (¬𝜓, false, 𝜈)

iff (i, j) is marked with (𝜓, true, 𝜈)

(45)

02917 Advanced

Topics in Embedded

Model checking: Case 𝜙 = ¬ 𝜓

Markings for (i , j):

∙ The true marking is (¬𝜓, true, 𝜇) iff (i, j) is marked with (𝜓, false, 𝜇)

∙ The false marking is (¬𝜓, false, 𝜈)

iff (i, j) is marked with (𝜓, true, 𝜈)

(46)

02917 Advanced

Topics in Embedded

Case 𝜓 = 𝜓 ₁ ^⌢ 𝜓 ₂ true marking

(k .j) : (𝜓

2

, true, 𝜇

₂

)

j (i, k) : (𝜓

1

, true, 𝜇

₁

)

i

k

(47)

02917 Advanced

Topics in Embedded

Case 𝜓 = 𝜓 ₁ ^⌢ 𝜓 ₂ true marking

(k .j) : (𝜓

2

, true, 𝜇

2

)

j (i, k) : (𝜓

1

, true, 𝜇

1

)

i

(i, j ) :(𝜓

1⌢

𝜓

₂

, true, 𝜇) k

where 𝜇 is

⋁ {

∃m

1

, m

2

: Split (k,m, m

1

, m

2

)

∧ ∀ m

1

, m

2

: Split (k,m, m

1

, m

2

) ⇒ (𝜇

1

[m

1

/m] ∧ 𝜇

2

[m

2

/m])

}

(48)

02917 Advanced

Topics in Embedded

Case 𝜓 = 𝜓 ₁ ^⌢ 𝜓 ₂ false marking

(k .j) : (𝜓

2

, false, 𝜈

₂

)

j

i

(i, k) : (𝜓

1

, false, 𝜈

₁

)

k

(49)

02917 Advanced

Topics in Embedded

Case 𝜓 = 𝜓 ₁ ^⌢ 𝜓 ₂ false marking

(k , j) : (𝜓

2

, false, 𝜈

2

)

j

i

(i, k) : (𝜓

1

, false, 𝜈

1

)

(i, j ) :(𝜓

1⌢

𝜓

₂

, false, 𝜈) k

where 𝜈 is C(i , j, m)∧ ⋀

∀ m

1

, m

2

: (Split (k, m, m

1

, m

2

) ⇒ 𝜈

1

[m

1

/m] ∨ 𝜈

2

[m

2

/m])

(50)

02917 Advanced

Topics in Embedded

Model checking 2: Example. Simplified markings

For dom m = {1, 2, 4} and 𝜁 = ∫

true < 4 ∧ ¬ ∫ p < 3.

Notice □( ∫

true < 4 ⇒ ∫

p < 3) ⇐⇒ ¬ ♢𝜁.

i, j C(m) markings (𝜓, false, 𝜂) for 𝜓 = after simplification ∫

true < 4 ¬ ∫

p < 3 𝜁 ♢𝜁 1,1 m[1] = m[2] m[1] > 2 m[1] < 3 true true 1,2 m[1] = m[2] + 1 m[1] > 2 m[1] < 3 true true 1,3 m[1] = m[2] > 0 m[1] > 1 m[1] < 3 true true 1,4 m[1] = m[2] > 0 m[1] > 1 ∨ m[4] > 0 m[1] ≤ 1 true true 2,{1, 3} m[2] = m[1] + 1 m[1] > 1 m[1] < 2 true true

. . .

3,{1, 2} false true true true true

3,3 true false true true true

. .

.

(51)

02917 Advanced

Topics in Embedded

Model checking 2: Example. Simplified markings

For dom m = {1, 2, 4} and 𝜁 = ∫

true < 4 ∧ ¬ ∫ p < 3.

Notice □( ∫

true < 4 ⇒ ∫

p < 3) ⇐⇒ ¬ ♢𝜁.

i, j C(m) markings (𝜓, false, 𝜂) for 𝜓 =

after simplification ∫

true < 4 ¬ ∫

p < 3 𝜁 ♢𝜁 1,1 m[1] = m[2] m[1] > 2 m[1] < 3 true true 1,2 m[1] = m[2] + 1 m[1] > 2 m[1] < 3 true true 1,3 m[1] = m[2] > 0 m[1] > 1 m[1] < 3 true true 1,4 m[1] = m[2] > 0 m[1] > 1 ∨ m[4] > 0 m[1] ≤ 1 true true 2,{1, 3} m[2] = m[1] + 1 m[1] > 1 m[1] < 2 true true

. . .

3,{1, 2} false true true true true

3,3 true false true true true

. .

.

(52)

02917 Advanced

Topics in Embedded

Summary

∙ Algorithm is correct.

∙ Procedure is 4-fold exponential.

∙ Size of generated formula is exponential in the chop-depth.

∙ Presburger formulas are checked in triple-exponential time.

Remember undecidable (non-elementary) starting point

∙ Preciseness when all chops is under same polarity and all conjunctions under the dual polarity.

∙ Quantifier elimination of side-condition is possible when all chops are in negative polarity. Procedure is then ”just” 2-fold exponential.

∙ Prototype is implemented by William Pihl Heise in a using the

solver Z3 as backend. The prototype has just been used on

small examples. Algorithm seems promising.

(53)

02917 Advanced

Topics in Embedded

Summary

∙ Algorithm is correct.

∙ Procedure is 4-fold exponential.

∙ Size of generated formula is exponential in the chop-depth.

∙ Presburger formulas are checked in triple-exponential time.

Remember undecidable (non-elementary) starting point

∙ Preciseness when all chops is under same polarity and all conjunctions under the dual polarity.

∙ Quantifier elimination of side-condition is possible when all chops are in negative polarity. Procedure is then ”just” 2-fold exponential.

∙ Prototype is implemented by William Pihl Heise in a using the

solver Z3 as backend. The prototype has just been used on

small examples. Algorithm seems promising.

(54)

02917 Advanced

Topics in Embedded

Summary

∙ Algorithm is correct.

∙ Procedure is 4-fold exponential.

∙ Size of generated formula is exponential in the chop-depth.

∙ Presburger formulas are checked in triple-exponential time.

Remember undecidable (non-elementary) starting point

∙ Preciseness when all chops is under same polarity and all conjunctions under the dual polarity.

∙ Quantifier elimination of side-condition is possible when all chops are in negative polarity. Procedure is then ”just” 2-fold exponential.

∙ Prototype is implemented by William Pihl Heise in a using the

solver Z3 as backend. The prototype has just been used on

small examples. Algorithm seems promising.

(55)

02917 Advanced

Topics in Embedded

Summary

∙ Algorithm is correct.

∙ Procedure is 4-fold exponential.

∙ Size of generated formula is exponential in the chop-depth.

∙ Presburger formulas are checked in triple-exponential time.

Remember undecidable (non-elementary) starting point

∙ Preciseness when all chops is under same polarity and all conjunctions under the dual polarity.

∙ Quantifier elimination of side-condition is possible when all chops are in negative polarity. Procedure is then ”just” 2-fold exponential.

∙ Prototype is implemented by William Pihl Heise in a using the

solver Z3 as backend. The prototype has just been used on

small examples. Algorithm seems promising.

(56)

02917 Advanced

Topics in Embedded