Automi temporizzati
w-linguaggi e w-automi (1)
Un w-linguaggio su un alfabeto finito S e’ un
sottoinsieme di Sw, l’insieme di tutte le stringhe
infinite su S.
Una tabella di transizione A e’ una quadrupla <S,S,S0,E>
dove
S alfabeto di input
S insieme finito di stati
S0S insieme di stati iniziali
E  SSS insieme di archi
w-linguaggi e w-automi (2)
L’automa descritto dalla tabella
- parte da uno stato iniziale,
- se <s,s’,a>E e si trova nello stato s leggendo
il simbolo a passa nello stato s’
Per una stringa s = s1 s2 s3 … su S
r = s0
s1
s1
s2
s2
s3
…
e’ un run di A su S purche’ s0S0 e <si-1,si,si>E per i1.
w-linguaggi e w-automi (3)
Per un run, l’insieme
inf(r) consiste degli stati sS tali che s=si per un
numero infinito di i0.
Automi di Büchi (1)
Un automa di Büchi e’ una tabella di transizione
<S,S,S0,E> con un insieme addizionale FS di stati di
accettazione.
Un run di A su una stringa sSw e’ un run di
accettazione se inf(r)F.
Almeno uno stato di accettazione deve essere ripetuto
infinite volte.
Automi di Büchi (2)
Il linguaggio accettato da A consiste delle stringhe
sSw tali che A ha un run di accettazione leggendo s.
s0
a,b
s1
a
a
L’automa accetta tutte le stringhe su {a,b} con un
numero finito di b.
Un w-linguaggio e’ regolare se e’ accettato da un
automa di Büchi.
Automi di Büchi (3)
s0
a
s1
b
b,c
s0
a
L1 dopo una occorrenza di a ci sono
occorrenze di b
a,c
s1
Sw – L1
a,c
a,b,c
Automi di Büchi (4)
s0
b,c
a
s1
a
b, c
s2
b, c
tra due occorrenze di a, c’e’ un numero pari di occorrenze di b e c
(anche zero)
Automi di Büchi (5)
Teorema
Se L da ASw e’ riconoscibile da un automa A
(regolare) allora lo e’ anche Sw –L.
Inoltre e’ possibile costruire l’automa per Sw –L.
Teorema
La classe degli w-linguaggi regolari e’ chiusa sotto le
operazioni booleane.
Automi di Büchi (6)
Teorema
E’ decidibile se il linguaggio riconosciuto da un automa
di Büchi e’ vuoto.
Teorema
E’ decidibile l’inclusione tra due w-linguaggi regolari L1
e L2.
Dimostrazione
Basta dimostrare che e’ vuota l’intersezione L1Sw-L2.
Automi di Büchi (7)
Un automa di Büchi A=<S,S,S0,E> e’ deterministico se e
solo se
- c’e’ un singolo stato iniziale (|S0|=1),
- il numero di archi etichettati da s, uscenti dallo stato
s, e’ al piu’ uno per tutti gli stati sS e tutti i simboli
sS.
La classe dei linguaggi riconosciuti dagli automi
deterministici e’ strettamente contenuta in quella degli
w-linguaggi regolari.
Automi di Büchi (8)
s0
a,b
s1
a
a
Non c’e’ nessun automa deterministico che riconosce
(a+b)*aw
Automi di Muller (1)
Un automa di Muller A e’ una tabella di transizione
<S,S,S0,E> con una famiglia di insiemi  di stati di
accettazione,  (S).
Un run di A su una stringa sSw e’ un run di
accettazione se inf(r) .
L’insieme di stati ripetuti infinite volte e’ uguale a un
insieme di .
Automi di Muller (2)
s0
b
s1
a
b
a
 = {{s1}}
Automa di Muller deterministico che riconosce (a+b)*aw
Teorema
La classe di linguaggi riconosciuta dagli automi di
Muller e’ la stessa di quella riconosciuta da quelli di
Büchi e da quelli di Muller deterministici.
Linguaggi temporizzati (1)
Modello del tempo: numeri reali non negativi, R.
Una sequenza temporale t = t1 t2 t3 … e’ una sequenza
infinita di valori tiR che soddisfa:
1. monotonicita’: t1 < t2 , i1.
2. progresso: per ogni t R c’e’ un i1 tale che ti > t.
Linguaggi temporizzati (2)
Una stringa temporizzata su S e’ (s,t) dove
s = s1 s2 s3 … e’ una stringa infinita su S e t e’ una
sequenza temporale.
Un linguaggio temporizzato su S e’ un insieme di
stringhe temporizzate su S.
Una stringa temporizzata puo’ essere vista come input
ad un automa. Il simbolo si e’ presentato al tempo ti.
Linguaggi temporizzati (3)
Il Linguaggio
L1={(s,t)| per ogni i, (ti>5.6)=>(si=a)}
su {a,b} e’ il linguaggio delle stringhe temporizzate in
cui non ci sono b dopo il tempo 5.6.
Il Linguaggio
L1={((ab)w,t)| per ogni i, (t2i- t2i-1) < (t2i+2- t2i+1)}
su {a,b} e’ il linguaggio delle sequenze di a e b in cui le
differenze tra i tempi delle a e delle b aumentano.
Linguaggi temporizzati (4)
Per un linguaggio L su S, Untime(L) e’ l’w-linguaggio
composto dalle stringhe s  Sw tali che per (s,t) L per
qualche sequenza temporale t.
Esempio
Untime(L1)=(a+b)*aw
Untime(L2)=(ab)w
Automi temporizzati (1)
La tabella di transizione e’ estesa a tabella di
transizione temporizzata.
Lo stato successivo dipende non solo dal simbolo letto,
ma anche dal tempo del simbolo letto rispetto ai tempi
dei simboli precedenti.
Alla tabella e’ associato un insieme di orologi. Un
orologio puo’ essere azzerato da una transizione.
In qualsiasi istante il valore di un orologio da’ il tempo
passato dal suo ultimo azzeramento.
Ogni transizione puo’ avere un vincolo sul valore degli
orologi.
Automi temporizzati (2)
s0
a, x:=0
s1
a, (x<2)?
L1={((ab)w,t)| per ogni i, t2i<t2i-1 + 2}
Automi temporizzati (3)
d, (y>2)?
s2
s1
s0
a, x:=0
b, y:=0
s3
c, (x<1)?
L1={((abcd)w,t)| per ogni i, (t4j+3<t4j+1 + 1) e (t4j+4>t4j+2 + 2) }
Automi temporizzati (4)
Dato un insieme di orologi X, l’insieme F(X) di vincoli
sugli orologi d e’ definito induttivamente come
d= xc | cx | d | d1  d2
c costante intera
Un’interpretazione n per un insieme di orologi X e’ una
funzione da X a R, n: X  R.
Una interpretazione n per X soddisfa un vincolo d se e
solo se d e’ valutato a “vero” per i valori dati da d.
Automi temporizzati (5)
Per t  R, n+t denota l’interpretazione che assegna a x
il valore n(x)+t .
Per YX, [Yt]n denota l’interpretazione che assegna
t a ciascun orologio yY e assegna n(z) a tutti gli
orologi zY.
Automi temporizzati (6)
Una tabella di transizione temporizzata A e’ data da
una quintupla <S,S,S0,C,E>, dove
S alfabeto di input
S insieme finito di stati
S0S insieme di stati iniziali
C insieme di orologi
E  SSS(C)F(C) insieme di archi
Una transizione e’ <s,s’,a,l,d> dove lC da’ l’insieme di
orologi che la transizione azzera.
Un automa di Büchi ha in piu’ l’insieme F degli stati di
accettazione.
Automi temporizzati (7)
s0
b
a
s2
s1
a, {x}
b, (x<2)
s3
a, {x}
L1={((ab)w,t)| per ogni i esiste ji: t2j<t2j-1 + 2}
Automi temporizzati (8)
a,b, x<3
s0
a, {x}, x=3
L1={(s,t)| per ogni i esiste ji: tj=3i e sj = a}
Automi temporizzati (9)
In un linguaggio temporizzato i simboli possono
essere arbitrariamente vicini
s0
a, {x}, x=1
s1
b, {y}
s2
a, {x}, x=1
s3
b, {y}, y<1
L1={((ab)w,t)|
per ogni i: (t2i-1=i) e (t2j - t2j-1 > t2j+2 -t2i+1)}
La differenza dei tempi di una a e la b successiva e’
strettamente decrescente.
Se non usassimo il tempo denso (R) per i tempi il
linguaggio sarebbe vuoto.
Automi temporizzati (10)
Un linguaggio temporizzato e’ regolare se esiste
un automa di Büchi temporizzato che lo accetta.
Teorema
La classe dei linguaggi regolari temporizzati e’
chiusa sotto l’unione e l’intersezione.
Teorema
Sia L un linguaggio temporizzato regolare.
Per ogni parola s, sUntime(L) se e solo se
esiste una sequenza t tale che tiQ per ogni i>1
e (s,t)L.
Gli automi non distinguono tra R e Q.
Automi temporizzati (11)
Teorema
Dato un automa di Büchi temporizzato A=
<S,S,S0,C,E,F>, e’ decidibile se il linguaggio
accettato da A e’ vuoto.
Teorema
Dato un automa di Büchi temporizzato A=
<S,S,S0,C,E,F>, e’ indecidibile se il linguaggio
accettato da A e’ l’insieme di tutte le stringhe
su S.
Teorema
Dati due automi A1 e A2, e’ indecidibile se
L(A1)L(A2).
Corollario
La classe dei linguaggi non e’ chiusa per
complemento.
Automi temporizzati (12)
Un automa temporizzato di Muller A= <S,S,S0,C,E,>
e’ una tabella di transizione temporizzata,
<S,S,S0,C,E>, piu’ una famiglia di insiemi (S).
Una stringa temporizzata e’ accettata se e solo se
l’insieme degli stati attraversati infinite volte
appartiene a .
Automi temporizzati (13)
s1
a, x<5
b, {x}
s0
a, x<2
s2
c, {x}
 e’ {{s0,s2}}
Ogni parola accettata dell’automa soddisfa:
1. s(a(b+c))* (ac)w
2. per ogni i1 (t2i-1 - t2i-2) e’ minore di 2 se il
simbolo di indice 2i e’ uguale a c, minore di 5
altrimenti.
Automi temporizzati (14)
Teorema
Un liguaggio temporizzato e’ accettato da un automa
temporizzato di Muller se e solo se e’ accettato da
un automa di Büchi.
Automi temporizzati (15)
Sia A= <S,S,S0,C,E,> un automa di Muller.
Notiamo che L(A)=F  L(AF) dove AF= <S,S,S0,C,E,{F}>, quindi e’
sufficiente costruire, per ogni insieme F, un automa di Büchi A’F che
accetta L(AF).
Assumiamo F={s1, s2, … sk}, l’automa A’F usa il non determinismo per
ipotizzare l’ingresso del ciclo in F. Quando in F, si usa un contatore per
assicurarsi che ogni stato e’ visitato infinite volte.
Gli stati di A’F sono della forma <s,i> dove i {0,1, … k}.
Per ogni transizione <s,s’,a,l,d> di A, l’automa A’F ha una transizione
<<s,0>,<s’,0>,a,l,d>. In aggiunta, se s’ F anche <<s,0>,<s’,1>,a,l,d>.
Per ogni transizione <s,s’,a,l,d> di A con s,s’ F, per ogni 1ik l’automa
A’F ha una transizione <<s,i>,<s’,j>,a,l,d> such that j=((i+1)mod k)+1 se
s=si, i=j altrimenti.
Il solo stato di accettazione e’ <sk,k>.
Automi temporizzati (16)
s0
a, x<5
s1
b, {x}
<s0,0>
a, x<5
a, x<2
s2

c, {x}
<s1,0>
a, x<2
b, {x}
<s2,0>
c, {x}
c, {x}
a, x<5
c, {x}
<s1,1>
c, {x}
a, x<2
<s2,1>
<s2,2>
a, x<2
e’ {{s1,s2}}
Automi temporizzati (17)
Data una tabella temporizzata <S,S,S0,C,E>, uno stato esteso
e’ dato da una coppia <s,n>, dove sS e n e’ una interpretazione
per i clock C.
In generale gli stati estesi sono infiniti, ma si possono
raggruppare in un numero finito di insiemi con le stesse
proprieta’.
Se per due stati estesi i valori clock hanno la stessa parte
intera e lo stesso ordinamento sulla parte frazionaria di tutti i
clock, allora i cammini a partire dai due stati sono gli stessi.
Dato tR, fract(t) denota la parte frazionaria e t la parte
intera. t = t +fract(t)
Automa delle regioni (1)
Sia A=<S,S,S0,C,E> una tabella temporizzata.
Per ogni xC sia cx la piu’ grande costante tale che xcx o xcx
occorre in E.
La relazione di ~ equivalenza e’ definita sull’insieme delle
interpretazioni per C: n~n’ se e solo se valgono le seguenti
condizioni:
1.
per tutti gli xC n(x) e n’(x) hanno lo stesso valore
oppure n(x) e n’(x) sono entrambi maggiori di cx
2. per tutti gli x,yC con n(x) cx e n(y) cy, fract(n(x)) 
fract(n(y)) se e solo se fract(n’(x))  fract(n’(y))
3. per tutti gli xC con n(x) cx, fract(n(x)) =0 se e solo se
fract(n’(x)) =0
Una “clock region” e’ una classe di equivalenza di ~, denotata [n]
Automa delle regioni (2)
Si consideri una tabella temporizzata con due orologi, x e y, e cx=2,
cy=1.
Regioni
y
6
14
8
1
0
1
2
x
vertici (es. [(0,1]))
segmenti (es. 0<x=y<1)
regioni (es 1<x<2  0<y<1 
fract(x)<fract(y))
Automa delle regioni (intuizione)
s2
b, y=1
a, {y}
s0
s1
c, x<1
c, x=1
d, x>2
s3
a, {y}, y<1
n(x)=1.5, n(y)=2.2
n’ (x)=1.5, n’(y)=1.9
y
n(x)=1.2, n(y)=0.9
n’ (x)=1.4, n’(y)=0.7
1
n(x)=1, n(y)=0.6
n’ (x)=1, n’(y)=0.4
0
1
2
x
Automa delle regioni (3)
Dato A=<S,S,S0,C,E> costruiamo l’automa delle regioni (A).
Uno stato di (A) consiste in uno stato di A e di una classe di
equivalenza del valore degli orologi.
L’idea e’ che quando A si trova nello stato esteso <s,n>, (A) si
trova nello stato ,s,[n]>.
Una regione a’ e’ un successore temporale della regione a se e
solo se per ogni na, esiste un tR, positivo, tale che n+ta’.
Automa delle regioni (4)
Costruiamo i successore temporali di una regione a.
Ricordiamo che una regione e’ definita da:
1. per ogni orologio un vincolo x=c, c-1<x<c oppure x>cx.
2. per ogni coppia x e y tale che c-1<x<c e d-1<y<d compaiono
in 1. l’ordine tra fract(x) e fract(y).
y
linea dei successori temporali
1
0
1
2
x
Automa delle regioni (5)
Prendiamo l’insieme C0 dei clock x tali che a soddisfa il vincolo x=c, con ccx.
Supponiamo C0 non vuoto.
La prima regione successore, b, di a e’ data da:
1.
per xC0, se a soddisfa x=cx b soddisfa x>cx altrimenti se a soddisfa x=c
b soddisfa c<x<c+1. Per per xC0, il vincolo in b e’ uguale a quello di a.
Le relazioni tra le parti frazionarie rimangono le stesse (per xC0 la parte
frazionaria era 0).
2.
y
1
0
1
2
x
Automa delle regioni (6)
Se il caso precedente non si applica, prendiamo l’insieme C0 dei clock x tali che
a non soddisfa x>cx e che hanno la parte frazionaria massima. Cioe’ per tutti gli
orologi y tali che a non soddisfa x>cx, fract(y)fract(x).
1.
per xC0, se a soddisfa c-1<x<c, b soddisfa x=c, Per per xC0, il vincolo in
b e’ uguale a quello di a.
Le relazioni tra le parti frazionarie rimangono le stesse.
2.
y
1
0
1
2
x
Automa delle regioni (6)
Dato A=<S,S,S0,C,E> il corrispondente automa delle regioni
(A) e’ definito nel modo seguente:
1.
Gli stati di (A) sono coppie <s,a> dove sS e a e’ una
regione.
2. Gli stati iniziali sono della forma <s0,[n0]> dove s0S0 e
n0(x)=0 per tutti gli orologi di C.
3. (A) ha un arco <<s,a>,<s’,a’>,a> se e solo se c’e’ un arco
<s,s’,a,l,d>E e una regione a’’ tale che (1) a’’ e’ un
successore temporale di a, (2) a’’ soddisfa d, e (3)
a’=[l0]a’’.
Automa delle regioni (7)
s2
b, y=1
a, {y}
s0
s1
c, x<1
c, x<1
d, x>1
s3
a, {y}, y<1
a
s0
a
x=y=0
a
s1
c
s3
0<y<x<1
b
s1
0=y<x<1
0=y, 1=x
a
a
s3
0<y<1<x
d
s1
0=y, 1<x
a
d
d
b
s2
1=y<x
b
d
a
d
s3
1=y<x
d
s3
d
1<y, 1<x
d
Automa delle regioni (8)
Per un automa temporizzato A=<S,S,S0,C,E>, il suo automa delle
regioni puo’ essere utilizzato per accettare Untime(L(A))
Teorema
Dato un automa temporizzato A=<S,S,S0,C,E>, esiste un automa
di Büchi su S che accetta Untime(L(A)).
L’automa delle regioni puo’ essere utilizzato per dimostrare che
il linguaggio accettato da un automa temporizzato e’ vuoto.
Ancora sugli automi temporizzati
Corollario
La classe dei linguaggi non e’ chiusa per complemento.
s0
a
a, {x}
s1
a
a, x=1
s3
a
L={(aw,t)| esiste i1: esiste j  i: tj=ti+1}
Ancora sugli automi temporizzati
Automi di Muller deterministici
Un automa temporizzato A=<S,S,S0,C,E> di Muller e’ deterministico se e solo
se
- ha solo uno stato iniziale |S0|=1
- per tutti gli sS, per tutti i sS, per ogni coppia di archi della forma
<s , _ , a , _ , d1> e <s , _ , a , _ , d2>, e sono mutamente esclusivi (d1 d2 e’
insoddisfacibile)
Teorema
La classe dei linguaggi accettati da automi deterministici di Muller e’ chiusa
per unione, intersezione e complemento.
Composizione parallela
A||A’ accetta la composizione di stringhe accettate da A e A’ in cui gli eventi
comuni avvengono allo stesso tempo
a, x=1,{x}
s0
s1
b
s0
a
c
s1
L={(a(bc+cb))w,t)| t3i-2=i}
Verifica di proprieta’ (1)
Si specifica il sistema mediante un automa temporizzato A.
Si specificano i comportamenti corretti mediante un automa temporizzato
deterministico P.
Si verifica che il linguaggio accettato da A e’ contenuto in quello accettato
da P.
Verifica di proprieta’ (2)
Un esempio: controllo di un passaggio a livello con tre componenti:
TRAIN
GATE
CONTROLLER
Il sistema e’ dato dalla loro composizione parallela
Verifica di proprieta’ (3)
idT
s0
approach, {x}
s1
in, x>2
exit, x<5
s3
out
TRAIN
s2
Verifica di proprieta’ (4)
idG
s0
lower, {y}
s1
up,
(y>1)  (y<2)
s3
down, y<1
raise, {y}
s2
idG
GATE
Verifica di proprieta’ (5)
idC
s0
approach, {z}
s1
raise, z<1
lower, z=1
s3
exit, {z}
s2
CONTROLLER
Verifica di proprieta’ (6)
~in, ~down
down
s0
~in, ~up
in
s1
up
~up, ~out
s2
out
Safety: quando in treno e’ nel passaggio a livello, questo
deve essere chiuso
Verifica di proprieta’ (7)
~down
down, {x}
s0
~up
s1
up, x<10
Liveness: il passaggio a livello non sta chiuso mai
per piu’ di dieci minuti
e transizioni
Aggiungendo le transizioni senza simboli si aumenta la potenza
del formalismo.
Non esiste nessun automa temporizzato senza transizioni e
che accetta il seguente linguaggio:
L1={(s,t)| per ogni i, ti(i,i+1] e
oppure
a, {x}, x=1
(ti=i+1 e si=a)
(ti(i,i+1) e si=b)}
b, 0<x<1
s0
s1
e, {x}, x=1