Modelli ed Equivalenze per la Valutazione Quantitativa di Sistemi Concorrenti

7/23/2019 Modelli ed Equivalenze per la Valutazione Quantitativa di Sistemi Concorrenti

1/34

Modelli ed Equivalenze per la Valutazione Quantitativa di

Sistemi Concorrenti

Tommaso Turchi

Universit degli Studi di Firenze

Facolt di Scienze Matematiche, Fisiche e NaturaliCorso di Laurea in Informatica

23 aprile 2010

Tommaso Turchi

Tommaso Turchi Modelli ed Equivalenze per la Valutazione Quantitativa di Sistemi Concorrenti


2/34

Outline

1 Motivazioni

2 Labelled Transition SystemsEquivalenza a tracceEquivalenza di testingBisimilarit

3 Rate Transition SystemsWeighed Trace EquivalenceWeighed Testing EquivalenceRate Aware Bisimilarity

4 Uniform Labelled Transition SystemsEquivalenza a tracceEquivalenza di testingBisimilarit

5 Conclusioni

ommaso Turchi



3/34

Motivazioni

Le algebre di processo sono state utilizzate con successo per modellare il

comportamento e validare propriet di sistemi concorrenti.

ommaso Turchi



4/34

Motivazioni



Ingredienti base di unalgebra di processo:

un insieme di operatori,

un modello per descriverne la semantica,

una nozione di equivalenza.

ommaso TurchiTommaso Turchi Modelli ed Equivalenze per la Valutazione Quantitativa di Sistemi Concorrenti


5/34

Motivazioni







LTS e SOS

CCS

CSP

ACP

. . .



6/34

Motivazioni







LTS e SOS

CCS

CSP

ACP

. . .

PEPATIPP

EMPA

. . .



7/34

Motivazioni







LTS e SOS

CCSCSP

ACP

. . .

RTS

PEPATIPP

EMPA

. . .



8/34

Motivazioni





un modello per descriverne la semantica,una nozione di equivalenza.

ULTraS

CCS

CSP

ACP

. . .

PEPA

TIPP

EMPA

. . .



9/34

Labelled Transition Systems

Definizione

Un Labelled Transition System S una tripla (S,A,) dove:S un insieme di stati,

A un insieme finito di azioni,

S A S una relazione ternaria detta relazione di transizione;

si denota con q

q quando (q, , q) .

Esempio

rotto

acceso spentooff

bang

on

bang



10/34

Equivalenze comportamentali

Come definiamo unequivalenza fra processi?

Tommaso TurchiTommaso Turchi Modelli ed Equivalenze per la Valutazione Quantitativa di Sistemi Concorrenti


11/34



Nozioni di equivalenza



12/34




Equivalenza a tracce identifica processi che effettuano le stessesequenze di azioni



13/34





Equivalenza di testing identifica processi indistinguibili per unosservatore esterno, cio un processo che interagisce col sistema solomediante composizione parallela



14/34






Bisimilarit identifica processi che sono in grado di simularsi lun con

laltro, dopo ogni passo di ogni loro computazione



15/34






Bisimilarit identifica processi che sono in grado di simularsi lun con

laltro, dopo ogni passo di ogni loro computazione

Proponiamo alcuni esempi.



16/34


Consideriamo un LTS e gli stati p, q e r.

p

p1

a

p2

b

p3

c

p4

d

q

q1

a

q2

b

q3

b

q4

c

q5

d

r

r1

a

r2

a

r3

b

r4

b

r5

d

r6

c

Problema: gli stati proposti sono equivalenti?


l l


17/34



p

p1

a

p2

b

p3

c

p4

d

trace

q

q1

a

q2

b

q3

b

q4

c

q5

d

trace

r

r1

a

r2

a

r3

b

r4

b

r5

d

r6

c

Sono equivalenti a tracce (T = {, a, ab, abc, abd})


E i l li


18/34



p

p1

a

p2

b

p3

c

p4

d

trace

test

q

q1

a

q2

b

q3

b

q4

c

q5

d

trace

test

r

r1

a

r2

a

r3

b

r4

b

r5

d

r6

c

Solo gli stati q e r sono testing equivalenti (considerare il test a?.b?.c?.)


E i l li


19/34



p

p1

a

p2

b

p3

c

p4

d

trace

test

bis

q

q1

a

q2

b

q3

b

q4

c

q5

d

trace

test

bis

r

r1

a

r2

a

r3

b

r4

b

r5

d

r6

c

Non sono bisimili (esiste una strategia vincente nel bisimulation game)


R t T iti S t


20/34

Rate Transition Systems

DefinizioneUn rate transition system R una tripla (S,A,) dove:

S un insieme di stati,

A un insieme di azioni,

S A [S R0] una relazione di transizione che associa aogni coppia stato-azione una funzione totale R : S R0.

La relazione di transizione associa a ogni coppia stato-azione (p, ) una

funzione totale (P, Q,. . . ) che assegna un numero reale non negativo aogni processo del sistema. Il valore 0 viene assegnato ai processi che nonsono raggiungibili da quello stato mediante lazione.


R t T iti S t


21/34

Rate Transition Systems

s3 s1 s2 s4

1

2

a

34

b5

6

7

8

p

P significa che, per un generico processo q:

se P(q) = x (= 0) allora q raggiungibile da p mediante lesecuzionedi , la cui durata esponenzialmente distribuita con rate x;

se P(q) = 0 allora q non raggiungibile da p mediante

Ogni nozione di equivalenza fra processi dovr tener conto dei rateassociati alle azioni nella propria valutazione.


W i h d T E i l


22/34

Weighed Trace Equivalence

Consideriamo un RTS e gli stati s1 e p1.

s1

a

s3

2

s2

1

b c

s4

s5

p1

a

p2

1 + 2

b c

p3

11+2

p4

21+2




23/34



s1

a

s3

2

s2

1

b c

s4

s5

trace

p1

a

p2

1 + 2

b c

p3

11+2

p4

21+2

Sono equivalenti a tracce pesate(wt(s1, a) = wt(p1, a), wt(s1, ab) = wt(p1, ab) e wt(s1, ac) = wt(p1, ac))


Weighed Testing Equivalence


24/34



s1

a

s3

2

s2

1

b b

s4

s5

p1

a

p2

1 + 2

b

p3

11+2

p4

21+2




25/34



s1

a

s3

2

s2

1

b b

s4

s5

test

p1

a

p2

1 + 2

b

p3

11+2

p4

21+2

Sono weighed testing equivalenti (mustt(s1, L) = mustt(p1, L) emustt({s1 after a}, L) = mustt({p1 after a}, L))


Rate Aware Bisimilarity


26/34


Consideriamo un RTS e gli stati s1 e s2.

s1a b

u1

1

u2

2

v1

1 + 2

c

w1

s2a b

u3

1 + 2

v2

1

v3

2

cc

w2




27/34


Consideriamo un RTS e gli stati s1 e s2.

s1a b

u1

1

u2

2

v1

1 + 2

c

w1

bis

s2a b

u3

1 + 2

v2

1

v3

2

cc

w2

Sono rate aware bisimili (S/R = {(s1, s2), (u1, u2, u3), (v1, v2, v3), (w1,w2)})


Uniform Labelled Transition Systems


28/34


Generalizzando ulteriormente la definizione di RTS si ottengono gli ULTraS.

Definizione

Sia D un ordine parziale completo. Un D-ULTraS R una tripla (S,A,)dove:

S un insieme di stati,

A un insieme di azioni,

S A [S D] una relazione di transizione.

Un LTS pu essere modellizzato come un D-ULTraS con D = B = {,}.

Un RTS pu essere modellizzato come un D-ULTraS dove D = R0.




29/34


Computazioni annotateSia R = (S,A,) un D-ULTraS, una computazione annotata unasequenza (A D).

AC(s) denota linsieme delle computazioni annotate che iniziano da s S.

Una computazione annotata AC(s) se e solo se:

= ;

= (a, v) ed esistono P e s tali che sa

P, P(s) = v = e AC(s).




30/34


Weighting function

Sia W un reticolo dove 0 denota il minimo e 1 il massimo. Una weightingfunction WD : S (A D)

2S W per un D-ULTraS S, A, misurail peso delle computazioni annotate da uno stato verso uninsieme di stati.

La weighting function WB per gli LTS definita in modo da ottenere:

WB(s, , S) =

1 se s raggiunge con uno stato in S,0 altrimenti.

La weighting function WR0 per gli RTS definita in modo da ottenere:

WR0 (s, , S) =

probabilit di raggiungere uno stato in S

con una computazione annotata da s.


Equivalenza a tracce


31/34



Sia (S, A,) un D-ULTraS e WD una weighting function.

Due stati s1, s2 S sono equivalenti a tracce se e solo se, per ognicomputazione annotata (A D):

WD(s1, , S) = WD(s2, , S)


Equivalenza di testing


32/34

q g

Insiemi Must

Sia R = (S,A,) un D-ULTraS, A A, s S e a A:

s must a se e solo se P = x. tale che sa

P;

s Must A se e solo se a A tale che s must a;

M(A

) = {s S | s Must A

}.

Equivalenza di testing

Sia (S, A,) un D-ULTraS e WD una weighting function.Due stati s1, s2 S sono testing equivalenti se e solo se, per ognicomputazione annotata (A D) e A A:

WD(s1, ,M(A)) = WD(s2, , M(A

))


Bisimilarit


33/34

Bisimulazione

Sia (S, A,) un D-ULTraS e WD una weighting function.Una relazione di equivalenza E S S una WD-bisimulation se e solose, per ogni (s1, s2) E, per ogni (A D)

e C S/E:

WD(s1, , C) = WD(s2, , C)

Bisimilarit

Due stati s1, s2 S sono WD-bisimili (s1 WD s2) se esiste una

WD-bisimulation E tale che (s1, s2) E.


Conclusioni


34/34

Teoremi di corrispondenza per gli LTS

Due stati sono equivalenti (tracce, testing o bisimili) su un LTS se e solo selo sono sul B-ULTraS corrispondente.

Teoremi di corrispondenza per gli RTS

Due stati sono equivalenti (tracce, testing o bisimili) su un RTS se e solose lo sono sul R0-ULTraS corrispondente.

Lavori futuri

Semantica delle algebre di processo mediante ULTraSSistemi temporizzati

Sistemi probabilistici


Modelli ed Equivalenze per la Valutazione Quantitativa di Sistemi Concorrenti

Documents

Transcript of Modelli ed Equivalenze per la Valutazione Quantitativa di Sistemi Concorrenti