Come ti sei comportato?
Equivalenze comportamentali e loro applicazioni
Daniele Gorla
Roma, 21 Settembre 2009
Sommario

Linguaggi di programmazione ed
equivalenze comportamentali

Dinamica e comportamento di canali di
comunicazione con energia consumabile
Linguaggi di programmazione

Sintassi (termini leciti)

Semantica (significato)
 Operazionale
(dinamica, implementazione)
Astrazione
 Comportamentale
(osservatore)
 Denotazionale
 Assiomatica
…
Equivalenze comportamentali

|[ - ]| associa a ogni programma il suo
comportamento

P ~ P’ sse |[ P ]| = |[ P’ ]|

Esempi:




Macchine di Turing: |[ P ]| è il linguaggio accettato da P
Ling. Funzionali: |[ P ]| è la funzione che calcola P
Ling. Non-deterministici: |[ P ]| è l’insieme delle
sequenze di azioni osservabili (tracce) che P produce
Ling. Imperativi: |[ P ]|μ è lo stato di memoria che P
produce partendo dallo stato di memoria iniziale μ
Applicazioni

Correttezza di programmi
Spec ~ Impl

Ottimizzazione del codice
Input ~ Output, ma Output è più efficiente

Proprietà di sicurezza




Riservatezza: s,s’. P(s) ~ P(s’)
Integrità
Autenticità
Correttezza di codifiche
E : Ling1 → Ling2 tale che P ~1 P’ sse E(P) ~2 E(P’)
Note dolenti

In generale, ~ è indecidibile




Equivalenza per linguaggi di MT
Equivalenza Morris-style per λ-termini
…
Per alcune equivalenze e con opportune restrizioni
sui programmi leciti, si passa al decidibile



Equivalenza per linguaggi di automi finiti
Equivalenza Morris-style per λ-calcolo tipato semplice
Equivalenza a tracce per processi non-deterministici a stati finiti

Di solito, la complessità computazionale non è
polinomiale (NPC, EXP, P-Space-C, …)

Tecniche di prova corrette (ma non complete)
polinomiali
Dinamica e comportamento di
canali di comunicazione con
energia consumabile
assieme a Pietro Cenciarelli e Ivano Salvo
4
4
3
2
7
9
2
6
4
3
4
5
4
2
4
3
2
7
9
1
2
6
4
3
4
5
2
4
3
2
2
7
9
1
6
4
3
3
4
5
2
4
2
1
2
7
9
8
1
6
5
3
3
4
5
2
4
1
2
1
7
8
1
0
5
3
2
3
4
5
2
4
1
1
0
7
6
8
0
5
4
2
0
3
4
5
2
4
3
1
0
7
6
0
5
4
0
3
4
5
Canale ()
2
source
3
1
0
7
6
4
target
0
0
3
4
5
Cammini (P )
2
Flusso ()
4
3
:P  N
2
7
che rispetta le energie di ogni vertice
9
1
Il valore di  è    = pP (p)
4
6
7
3
4
5
Esempio di Flusso
4
4
3
(
)= 2
(
)= 1
= 3
2
7
9
1
6
7
3
4
5
Transizioni
4
4
3
4
2
4
0
0
7
9
7
5
6
1
7
4
3
5
(
)= 2
(
)= 1
= 3
0
2
2
3
4
4
Tracce
2
5
1
3
...
2
Una traccia di un canale  è una sequenza n1, n2 ... t.c.
n1
n2
      ...
Tracce

(
5
2
1
) =3 2, 1 , 2, 1, 2 ,21, 1, 1, 1 , 5. ., ....
Una traccia di un canale  è una sequenza n1, n2 ... t.c.
n1
n2
      ...
() è l’insieme delle computazioni di 
Equivalenza (  )
2
5
?!

5
4
   sse () = ()
Teor:    sse max() = max()
( facile )
2
5
4
Equivalenza (  )
2
5
2
5
4
4
Equivalenza (  )
2
4
5

4
2
2
0
4
5
2
4

1
0
Equivalenza ( ? )
2
5
5
4
2
Una traccia5(completa) di un canale  è una sequenza n1 , ... , nk t.c.
n
n
1
k
 4 ... 

tr() è l’insieme delle tracce complete
Equivalenza ( tr )
2
tr
2
≁tr
5
5
4
5
4
Una traccia (completa) di un canale  è una sequenza n1 , ... , nk t.c.
n1
nk
  ... 

tr() è l’insieme delle tracce complete
 tr  sse tr() = tr()
Equivalenza ( tr )
2
tr
2
≁tr
5
5
5
4
4
mif = 5
mif = 5
mif = 4
mif() è il valore del minimum inhibiting flow di 
Teor:  tr  sse max() = max() e mif() = mif()
( difficile )
Complessità ( tr )
max() è polinomiale
mif() NPC
?
ridurre MinMaxMatching in un grafo bipartito
di grado al più 3 a MIF
Altre possibili equivalenze?
1
1
2
tr
1
3
1
1
mif = 2
max = 3
mif = 2
max = 3
Altre possibili equivalenze?
1
1
2
tr
1
3
1
1
mif = 2
max = 3
mif = 2
max = 3
Altre possibili equivalenze?
1
0
1
2
2
1
1
1
1
3
1
1
2
Altre possibili equivalenze?
1
2
≉
1
1
  tr
3
1 (bisimulazione)
1
Sviluppi futuri
• Studio della bisimulazione
• caratterizzazione
• complessità
• Modello più sofisticato
(fallimenti, strategie di routing, …)
• Problemi di ottimizzazione
(es: caratterizzazione di reti che soffrono del paradosso di Braess)