Che materia stai cercando?

# Embedded Systems - Formal methods to the analysis and control

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. Vedi di più

Esame di Sistemi embedded docente Prof. L. Pomante

Anteprima

### ESTRATTO DOCUMENTO

Example: Software

Assume that we are interested in knowing if x is smaller, equal, or greater

than 1 when y is restricted to assume values in the set {1,2}. One possible

finite-state model capturing the dynamics of x is represented in the

following:

Taken from Tabuada, Verification and Control of Hybrid Systems, Springer Verlag, 2009.

Embedded Systems

A unified framework: continuous processes

Given a control system Σ:

, x R , u R

n m

∈ ∈

we can define the following LTS

T(Σ) = (Q,L,⎯→,O,H),

where:

Q = R n

 L is the collection of control signals u : R R m

 →

u

p q, if x(τ,p,u) = q for some 0

 ⎯→ τ ≥

O = R n

 H is the identity function

T(Σ) captures all information contained in Σ

… by using similar arguments I can associate a LTS to a hybrid system!

Embedded Systems

A unified framework: continuous processes

Given a control system Σ:

, x R , u R

n m

∈ ∈

we can define the following LTS

T(Σ) = (Q,L,⎯→,O,H),

where: p q = x(τ,p,u)

Q = R n

 L is the collection of control signals u : R R m

 →

u

p q, if x(τ,p,u) = q for some 0

 ⎯→ τ ≥ u

O = R n

 p q

H is the identity function

T(Σ) captures all information contained in Σ

… by using similar arguments an LTS can be associated to a hybrid system!

Embedded Systems

A unified framework

Given a control system Σ:

, x R , u R

n m

∈ ∈

we can define the following LTS

T(Σ) = (Q,L,⎯→,O,H),

where: p q = x(τ,p,u)

Q = R n

 L is the collection of control signals u : R R m

 →

u

p q, if x(τ,p,u) = q for some 0

 ⎯→ τ ≥ u

O = R n

 p q

H is the identity function

T(Σ) captures all information contained in Σ

… by using similar arguments I can associate a LTS to a hybrid system!

Embedded Systems

Language equivalence

Definition T and T are language equivalent if L(T ) = L(T )

1 2 1 2

L( ) = L( )

b a

a a b

q

q q q

q

3

2

1 2 3 5

4

• Same language implies same evolution of predicates we are interested in

analyzing

Embedded Systems

Language equivalence

Definition T and T are language equivalent if L(T ) = L(T )

1 2 1 2

L( ) = L( )

b a

a a b

q

q q q

q

3

2

1 2 3 5

4

Language equivalence is an equivalence relation

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

• Same language implies same evolution of predicates we are interested in

(reflexivity) L(T ) = L(T )

 analyzing 1 1

(symmetry) L(T ) = L(T ) L(T ) = L(T )

 ⇒

1 2 2 1

(transitivity) L(T ) = L(T ) L(T ) =L(T ) L(T ) = L(T )

 ∧ ⇒

1 2 2 3 1 3

Embedded Systems

Bisimulation equivalence

R. Milner (1989), Communication and Concurrency. Prentice Hall

D.M.R. Park (1981), Concurrency and automata on infinite sequences. LNCS, vol. 104

... the intuitive idea!

T l l

2

1 3

1 4 l

l

Embedded Systems

Bisimulation equivalence

R. Milner (1989), Communication and Concurrency. Prentice Hall

D.M.R. Park (1981), Concurrency and automata on infinite sequences. LNCS, vol. 104

… the intuitive idea!

T l T

l

2

1 2

l l

is bisimilar to

3

1 7

6

5

4 l

l

Embedded Systems

Bisimulation equivalence

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

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

O = O , a relation

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 H (p ) = H (p )

 ⎯→ ⎯→

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

l

l 1

2

q p in T implies existence of q p in T so that H (p ) = H (p )

 ⎯→ ⎯→

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

T l T

l

2

1 2

l l

is bisimilar to

3

1 7

6

5

4 l

l

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

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

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 R = { (1,5), (2,6), (3,7), (4,6) }

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 ( ) = ?

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

π|

Q1

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 ( ) = { 1, 2, 3, 4 }

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

π|

Q1

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 ( ) = ?

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

PAGINE

72

PESO

679.08 KB

AUTORE

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!

Dispensa

Dispensa

Dispensa

Dispensa