Metodi formali nel
progetto
dell’interazione
Anna Labella
Due aspetti
• La struttura del tempo
• Il tipo di interazione
la struttura del tempo
Tempo discreto
Tempo continuo a gradini
Tempo continuo
Qual’è più “facile” e quale più utile?
Il tipo di interazione
Handshaking
Broadcasting
“a braccetto”
Controllo
Rilevamento di segnale
Rendez-vous
ecc.
Esempi tratti dall’interazione
Combinazione di diversi processi
Per mezzo di rendez-vous
Esempi tratti dall’interazione
Interfacce come tipici esempi di
coesistenza di diversi “tipi di tempo”
Cosa ci interessa e cosa no
Eventi che si svolgono e/o si evolvono in un intervallo di tempo
Eventi che devono aspettare input dall’esterno
Latenze in informatica musicale
Interpretazione legata alle durate (es. doppio click)
Eventi istantanei
Eventi a distanza sempre più ravvicinata
Il problema cruciale:
l’interpretazione
Riconoscimento di comportamento
Una possibile soluzione:
diversi livelli di astrazione
Linee guida per disegnare interfacce ibride continue
Mieke Massink Giorgio P. Faconti,
A reference framework for continuous interaction
UAIS, 1 (2002) 237-251
http://www.springerlink.com/index/10.1007/s10209-002-0027-5
• fisico
• percettivo
• proposizionale
• concettuale
• di gruppo
Gestire l’interazione
trasformando l’informazione dai
sensori agli effettori
Philip Barnard, Jon May, David Duke, David Duce
Systems, interactions, and macrotheory
ACM TOCHI,7 (2000) 222--262
http://doi.acm.org/10.1145/353485.353490
Gli automi ibridi
Una soluzione?
Thomas A. Henzinger,
The Theory of Hybrid Automata,
Proc. 11th LICS Conf. (1996) 278-292
Automa ibrido
X
(V,E)
init, inv, flow
jump

<X,(V,E), init, inv, flow, jump, , E   >
n-uple di variabili reali,
grafo di controllo, modalità ed interruttori
condizioni che etichettano le modalità
condizione che etichetta gli interruttori
eventi
Gli automi ibridi
Una soluzione?
Thomas A. Henzinger,
The Theory of Hybrid Automata,
Proc. 11th LICS Conf. (1996) 278-292
Sistema di transizione temporizzato
Q,Q0 V Rn,
<Q,Q0,A,  >
(v,x)Q sse inv(v)[X:=x] vero
(v,x)Q0 sse inv(v)[X:=x] e init(v)[X:=x] veri
A=R+
eventi e durate
:(v,x)  (v’,x’) sse c’è
e E v  v’
jump(e)[X,X’:=x,x’]
event(e)=
:(v,x)  (v,x’) sse c’è
f:[0,  ]  Rn differenziabile
f(0) = x f() = x’
inv(v) [X:= f() ]
0≤≤
flow(v ) [X, •X:= f(), •f()] veri
Marionette virtuali
Il sistema
All’esterno è un processo veramente continuo, almeno a tratti,
che viene rilevato secondo certi intervalli di tempo dai sensori.
Questi innescano delle procedure all’interno costanti,
ma su intervalli di tempo reali (almeno in prima approssimazione).
Esistono uno o più sistemi temporali sia interni che esterni.
Descrizione del sistema interno
Usare soltanto durate e
corrispondenze temporali
Non ci domandiamo perché e come accadano certe transizioni,
Ma le osserviamo
Osservabilità e nondeterminismo
Un processo può essere descritto osservando il suo
comportamento dall’esterno.
Non è detto che la stessa osservazione porti nello stesso stato
È suggerita una struttura ad albero
a
d
b c
a
b
c
La nozione di processo
a.P a P
ed altri operatori…..
Pi  a Qi

P1+P2  a Qi
Il tempo discreto
0
1
2
3
4
N
A = {a,b,c,d,…}
aacb
Alberi discreti
0
1
2
3
N
Set
Il tempo continuo a gradini
0
r1
r2
r3
r4
R+
A = {a,b,c,d,…}
(a,r1 ) (a,r2 - r1 ) (c, r3 - r2 ) (b, r4 - r3 )
Il tempo continuo
0
r1
r2
r3
r4
R+
F = {f,g,h,k,…}
(f |r1 ) (f |r2 - r1 ) (h |r3 - r2 ) (g |r4 - r3 )
Alberi continui
0
r1
r2
r3
r4
R+
Set
Le categorie di alberi
Un albero è un insieme di cammini etichettati ed incollati
lungo un’etichetta che è un prefisso comune.
Questo significa che, a sua volta un albero è una categoria
arricchita su una 2-categoria localmente posetale L
Un morfismo di L-alberi è un L-funtore: una funzione tra
cammini che rispetta strettamente l’etichettatura e può far
crescere l’incollamento, cioè una simulazione che tende a
diminuire il non determinismo
Gli alberi
t = (X, e, d) :
i. un insieme di cammini: X
ii. una funzione etichettatura e: X  L,
ii. una funzione incollamento d : X  X  L
t.c. per ogni x, y, z in X,
-
d (x, x) = e(x)
d(x, y) ≤ e (x)  e (y)
d(x, y)  d(y, z) ≤ d(x, z)
d (x, y) = d (y, x)
Un morfismo f : t1  t2
è una funzione f : X1 X2
tale che
i.
e2 (f(x)) = e1 (x)
ii.
d1 (x, y) ≤ d2 (f(x), f(y))
a
b c
a
c b
a
a
b
b
c
a
b
c
Operazioni tra alberi
Somma:
t1 + t2 = < X, e, d> , dove
- X = X1  X2
- e (x1) = e1 (x1)
- e (x2) = e2 (x2)
- d ( x, y)
=
•0 = <Ø , Ø , Ø>
 di (x, y) se x, y Xi


altrimenti
è l’unità
Esempio

Operazioni tra alberi
Concatenazione:
t1  t2 = < X, e, d> , dove
- X = X1  X2
- e (< x1, x2 >) = e1 (x1) . e2 (x2)
 d1 (x1, y1).d2 (x2, y2) se x1 = y1
- d (< x1, x2 >, < y1, y2 >) = 
 d1 (x1, y1)
altrimenti
•1 = <{ x } , e (x) =  , d (x, x) = > is l’elemento neutro
•Tree(A) monoidale chiusa a destra
•La concatenazione distribuisce a destra sulla somma
Esempio

Esempi di 2-categorie di base: le strutture temporali
•A* monoide libero sull’alfabeto A, funzioni parziali da N ad A
•CA funzioni parziali costanti a gradino da R+ ad A
•CF funzioni parziali continue a tratti
•TA monoide a tracce, ecc.
In generale: L monoide che sia anche un inf-semireticolo
Più in generale sistemi di tracce con rendez-vous (vedremo più avanti)
Il tempo non completamente ordinato
Etichettatura con tracce di Mazurkiewicz: A*/I
Parole con possibilità di invertire certe lettere [a,b]
c
[a,b]
b
c
Sincronizzazione e fusione
Tempo globale: Sincronizzazione
Tempi relativi: Rendez-vous
Sincronizzazione
t1 ※ t2 = < X, e, d> , dove
- X  X1  X2
- e (< x1, x2 >) = e1 (x1) * e2 (x2)
- d (< x1, x2 >, < y1, y2 >) = (e1 (x1) * e2 (x2))  (e1 (y1) * e2 (y2))
Tagliato eventualmente alla lunghezza minima tra d1(x1, y1) e d2(x2, y2)
Definiamo una tabella di sincronizzazione per coppie di mosse
“contemporanee” e costruiamo l’albero che viene etichettato con i
risultati.
La sicronizzazione può essere: handshaking, a braccetto, ecc.
Esempio
a
a
a
a
b
c
※
d
d
a
a
b
d
b
Fusione
Etichettatura sui prefissi,
ma incollamento su opportuni sottoinsiemi:
Ogni sottoprocesso ha il suo tempo
Una nuova struttura di frecce tra le parole
Fusione tra alberi (caso discreto)
(X, e, d)  (X’, e’, d’) :
i. un insieme di cammini: X  X’
ii. una funzione etichettatura e  e’: X  X’  A *,
ii. una funzione incollamento  : X  X’  ANN
t.c. per ogni x, y in X, x’, y’ in X’
-
 (x,x’) s.i. consistente di e(x) e di e(x’)
d (y, x)   (x,x’)   (y,x’)
 (x,x’)  d’(x’, y’)   (x,y’)
 (x, x’) =  (x’, x)
Notare l’analogia con la nozione di albero
In realtà sono cambiate soltanto le frecce della categoria di base:
Gli oggetti continuano ad essere prefissi,
le frecce sono soltanto insiemi consistenti
x
e(x)
a(x,y)
y
e(y)
Arricchimenti doppi
Coesistenza di due tipi di tempo
Loro sincronizzazione per prefisso
Caso di comportamento ibrido
t = (X, e, d) :
i. un insieme di cammini: X
ii. una funzione etichettatura e: X  CF  CA,
cioè e-: X  CF ed e+: X  CA
iii. per ogni x, y in X una funzione incollamento monotona
dx,y : [e-(x), e-(y) ]  [e+(x), e+(y) ]
t.c. per ogni x, y, z in X,
-dx,x [e-(x), e-(x) ]  [e+(x), e+(x) ] rispetta il massimo
- d(x, y) ≤ e (x)  e (y)
- dx,y  dy,z ≤ dx,z
- dx,y = dy,x
Attenzione!
la situazione non è simmetrica
rispetto alle due etichettature
Da una parte dobbiamo prendere tutti i prefissi comuni, dall’altra no:
questo vuol dire che abbiamo nondeterminismo soltanto a destra.
Si potrebbe generalizzare prendendo relazioni al posto di funzioni
Esempio
e-(x) = (f |r1 ) (f |r2 - r1 ) (h |r3 - r2 ) (g |r4 - r3 )
e+(x) = (a,s1 ) (a,s2 - s1 ) (c, s3 - s2 ) (b, s4 - s3 )
e-(x)
e+(x)
x
e-(y) = (f |r1 ) (f |r2 - r1 ) (h |r’3 - r2 ) (k |r’4 - r’3)
e+(y) = (a,s1 ) (a,s2 - s1 ) (c, s’3 - s2 ) (d, s’4 - s’3 )
e-(y)
e+(y)
y
dx,x [e-(x), e-(x) ]  [e+(x), e+(x) ] potrebbe essere indotta
dalla funzione sugli istanti di tempo {ri}  {si}, così
dx,y [e-(x), e-(y) ]  [e+(x), e+(y) ]
A che servono i metodi formali?
A che servono i metodi formali?
Servono a capire
Vengono prima o dopo la pratica?
Si intercalano