Che materia stai cercando?

Anteprima

ESTRATTO DOCUMENTO

Bisimulation equivalence

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a bisimulation relation between T and T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

l

l 1

2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T and T are bisimilar, denoted T , if (R) = Q and (R) = Q

∼T π| π|

1 2 1 2 Q1 1 Q2 2

T l T

l

2

1 2

l l

3

1 7

6

5

4 l

l ( ) = ?

R = { (1,5), (2,6), (3,7), (4,6) }

π|

Q2

Embedded Systems

Bisimulation equivalence

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a bisimulation relation between T and T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

l

l 1

2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T and T are bisimilar, denoted T , if (R) = Q and (R) = Q

∼T π| π|

1 2 1 2 Q1 1 Q2 2

T l T

l

2

1 2

l l

3

1 7

6

5

4 l

l ( ) = { 5, 6, 7 }

R = { (1,5), (2,6), (3,7), (4,6) }

π|

Q2

Embedded Systems

Bisimulation equivalence

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a bisimulation relation between T and T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

l

l 1

2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T and T are bisimilar, denoted T , if (R) = Q and (R) = Q

∼T π| π|

1 2 1 2 Q1 1 Q2 2

Bisimulation equivalence

preserves

most of the dynamical properties

of interest!

Embedded Systems

Bisimulation equivalence

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a bisimulation relation between T and T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

l

l 1

2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T and T are bisimilar, denoted T , if (R) = Q and (R) = Q

∼T π| π|

1 2 1 2 Q1 1 Q2 2

Bisimulation equivalence is an equivalence relation

on the space of transition systems, i.e. :

(reflexivity) T

 ∼T

1 1

(symmetry) T T

 ∼T ⇒ ∼T

1 2 2 1

(transitivity) T T T

 ∧ ⇒

∼T ∼T ∼T

1 2 2 3 1 3

Embedded Systems

Bisimulation equivalence

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a bisimulation relation between T and T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

l

l 1

2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T and T are bisimilar, denoted T , if (R) = Q and (R) = Q

∼T π| π|

1 2 1 2 Q1 1 Q2 2

Bisimulation equivalence is an equivalence relation

on the space of transition systems, i.e. :

(reflexivity) T

 ∼T

1 1

(symmetry) T T

 ∼T ⇒ ∼T

1 2 2 1

(transitivity) T T T

 ∧ ⇒

∼T ∼T ∼T

1 2 2 3 1 3 … what is R in the three cases?

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 T* is minimal!

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 T* is minimal!

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 T* is minimal!

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 T* is minimal!

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive (not all bisimulation relations are so!)

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 T* is minimal!

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 T* is minimal!

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 T* is minimal!

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 a b

C C

1 2

T* is minimal!

 T*

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

b b a

a

T q

a q

q q q 5

3

1 2 4

Maximal bisimulation relation between T and T:

R* = {(q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ), (q ,q ),

1 1 2 2 3 3 4 4 5 5 1 3 3 1 1 5 5 1 3 5

(q ,q ), (q ,q ), (q ,q )}

5 3 2 4 4 2

Maximal bisimulation relation is an equivalence relation on Q,

i.e. it is reflexive, symmetric and transitive

Construct equivalence classes induced by R*, i.e. C = {q ,q ,q } and C = {q ,q }

 1 1 3 5 2 2 4

Partition the state space of T as Q = C C

 ∪

1 2

Construct the quotient T* of T induced by R*, i.e.

 a b

C C

1 2

T* is minimal!

 T*

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

The core problem is the computation of R*? How?

B(0) = { (q,p) Q x Q s.t. H(q) = H(p) }

B(k+1) = { (q,p) Q x Q s.t.

q q’ p p’ s.t. (q,p) B(k)

∀ ⎯→ ∃ ⎯→ ∈ ∧

p p’ q q’ s.t. (q,p) B(k) }

∀ ⎯→ ∃ ⎯→ ∈

If k* s.t. B(k*) = B(k*+1) then R* = B(k*)

If Q is finite termination of the algorithm is guaranteed in polynomial time!

If Q is infinite (as in the case of control systems) …

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

The core problem is the computation of R*? How?

B(0) = { (q,p) Q x Q s.t. H(q) = H(p) }

B(k+1) = { (q,p) Q x Q s.t.

l l’

q q’ p p’ s.t. (q’,p’) B(k)

∀ ⎯→ ∃ ⎯→ ∈ ∧

l’

l

p p’ q q’ s.t. (q’,p’) B(k) }

∀ ⎯→ ∃ ⎯→ ∈

If k* s.t. B(k*) = B(k*+1) then R* = B(k*)

If Q is finite termination of the algorithm is guaranteed in polynomial time!

If Q is infinite (as in the case of control systems) …

Embedded Systems

Bisimulation equivalence

Bisimulation as a tool for reduction:

The core problem is the computation of R*? How?

B(0) = { (q,p) Q x Q s.t. H(q) = H(p) }

B(k+1) = { (q,p) Q x Q s.t.

l l’

q q’ p p’ s.t. (q’,p’) B(k)

∀ ⎯→ ∃ ⎯→ ∈ ∧

l’

l

p p’ q q’ s.t. (q’,p’) B(k) }

∀ ⎯→ ∃ ⎯→ ∈

If k* s.t. B(k*) = B(k*+1) then R* = B(k*)

If Q is finite, termination of the algorithm is guaranteed in polynomial time!

If Q is infinite, (as in the case of control systems) …

Embedded Systems

Language and bisimulation equivalence

L(T ) = L(T )

T ∼T 1 2

1 2

Embedded Systems

Language and bisimulation equivalence

L(T ) = L(T )

T ∼T 1 2

1 2

Embedded Systems

Bisimulation equivalence

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a bisimulation relation between T and T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

l

l 1

2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T and T are bisimilar, denoted T , if (R) = Q and (R) = Q

∼T π| π|

1 2 1 2 Q1 1 Q2 2

Bisimulation equivalence

preserves

most of the dynamical properties

of interest!

Embedded Systems

Abstraction and simulation

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

simulation from to

is a bisimulation relation between T and T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

l

l 1

2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T and T are bisimilar, denoted T , if (R) = Q and (R) = Q

∼T π| π|

1 2 1 2 Q1 1 Q2 2

T T

is simulated from T ≤

1 2

2 Bisimulation equivalence

preserves

most of the dynamical properties

of interest!

Embedded Systems

Abstraction and simulation

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a simulation relation from T to T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T is simulated from T , denoted T T , if (R) = Q

≤ π|

1 2 1 2 Q1 1

Bisimulation equivalence

preserves

most of the dynamical properties

of interest!

Embedded Systems

Abstraction and simulation

Given T = (Q ,L ,⎯→ ,O ,H ) and T = (Q ,L ,⎯→ ,O ,H ) with O = O , a relation

1 1 1 1 1 1 2 2 2 2 2 2 1 2

R Q × Q

⊆ 1 2

is a simulation relation from T to T if for all (q , q ) R

1 2 1 2

H (q ) = H (q )

 1 1 2 2 l

l 2

1

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

1 1 1 1 2 2 2 2 1 2

q p in T implies existence of q p in T so that (p , p ) R

 ⎯→ ⎯→ ∈

2 2 2 2 1 1 1 1 1 2

LTSs T is simulated from T , denoted T T , if (R) = Q

≤ π|

1 2 1 2 Q1 1

Simulation relation is not equivalence relation

on the space of transition systems, but :

(reflexivity) T T

 ≤

1 1

(symmetry) T T T T

 ≤ ≤

1 2 2 1

(transitivity) T T T T T T

 ≤ ∧ ≤ ⇒ ≤

1 2 2 3 1 3

Embedded Systems

Language inclusion and simulation relation

L(T ) L(T )

T T ⊆

≤ 1 2

1 2

Embedded Systems

Simulation relation and bisimulation equivalence

T T T T T T

∼ ≤ ∧ ≤

1 2 1 2 2 1

Embedded Systems

Abstraction and simulation

b b a

a

T

1 q

a q

q q q 5

3

1 2 4

b a

a

T q

q q

2 8

6 7

a b

T q q

3 9 10

Embedded Systems

Abstraction and simulation

b b a

a

T

1 q

a q

q q q 5

3

1 2 4

T T

1 2 b a

a

T q

q q

2 8

6 7

T T

2 3 a b

T q q

3 9 10

Embedded Systems

Abstraction and simulation

b b a

a

T

1 q

a q

q q q 5

3

1 2 4

T T

1 2 b a

a

T q

q q

2 8

6 7

T T

2 3 a b

T q q

3 9 10 … who is R in the two cases?

Embedded Systems

Abstraction and simulation

b b a

a

T

1 q

a q

q q q 5

3

1 2 4 Asbstraction

T T

1 2 Refinement

b a

a

T q

q q

2 8

6 7

T T

2 3 a b

T q q

3 9 10

Embedded Systems

Abstraction and simulation

b b a

a 5 states

T

1 q

a q

q q q 5

3

1 2 4 Asbstraction

T T

1 2 Refinement

b a

a

T q 3 states

q q

2 8

6 7

T T

2 3 a b

T 2 states

q q

3 9 10

Embedded Systems

Abstraction and simulation

T … infinite number of states…

0 b b a

a 5 states

T

1 q

a q

q q q 5

3

1 2 4 Asbstraction

T T

1 2 Refinement

b a

a

T q 3 states

q q

2 8

6 7

T T

2 3 a b

T 2 states

q q

3 9 10

Embedded Systems

Abstraction and simulation

T … infinite number of states…

0 b b a

a 5 states

T

1 q

a q

q q q 5

3

1 2 4

T T

1 2 b a

a

T q 3 states

q q

2 8

6 7

T T

2 3 a b

T 2 states

q q

3 9 10 Why abstraction?

Embedded Systems


PAGINE

72

PESO

679.08 KB

AUTORE

Atreyu

PUBBLICATO

+1 anno fa


DESCRIZIONE DISPENSA

Contents:
- A unified framework;
- A printer data buffer;
- A slot machine;
- Modeling recap;
- A unified framework: discrete processes;
- Example: software;
- A unified framework: continuous processes;
- Language equivalence;
- Bisimulation equivalence.


DETTAGLI
Corso di laurea: Corso di laurea magistrale in ingegneria delle telecomunicazioni
SSD:
Università: L'Aquila - Univaq
A.A.: 2011-2012

I contenuti di questa pagina costituiscono rielaborazioni personali del Publisher Atreyu di informazioni apprese con la frequenza delle lezioni di Sistemi embedded e studio autonomo di eventuali libri di riferimento in preparazione dell'esame finale o della tesi. Non devono intendersi come materiale ufficiale dell'università L'Aquila - Univaq o del prof Pomante Luigi.

Acquista con carta o conto PayPal

Scarica il file tutte le volte che vuoi

Paga con un conto PayPal per usufruire della garanzia Soddisfatto o rimborsato

Recensioni
Ti è piaciuto questo appunto? Valutalo!

Altri appunti di Sistemi embedded

Programmazione concorrente
Dispensa
Sistemi Embedded
Dispensa
SystemC
Dispensa
Real-time and embedded operating systems
Dispensa