Automi temporizzati
Automi e Linguaggi Formali
• Vari tipi di macchine a stati finiti (automi) e
relazioni con le grammatiche
• Classi di linguaggi, la gerarchia di Chomsky
• Applicazioni importanti di questi risultati teorici:
compilatori, parser…..
Automi e Verifica di Sistemi
• Gli automi sono utilizzati anche in molti metodi
formali (e realtivi tool) per la verifica di sistemi
per esempio tramite la specifica di proprieta’ con
logiche temporali
• Varie estensioni per modellare sistemi concorrenti
e distribuiti
• Automi concorrenti, cooperanti, gerarchici
• Non avremo tempo di studiare questi modelli
(argomenti di seminari)
Automi Temporizzati
• L’obiettivo e’ di avere uno strumento di specifica
per sistemi real-time, il cui comportamento
dipende da vincoli temporali
• Si estendono gli automi a stati finiti (in realta’ gli
automi su stringhe infinite) con una nozione di
tempo continuo
• Rajeev Alur and David L. Dill, A Theory of Timed
Automata, Theoretical Computer Science
126:183-235, 1994.
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 etichettati
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)
Sugli automi di Buchi sono state studiate tutta una
serie di proprieta’ ed algoritmi (che estendono i
risultati visti per i linguaggi regolari)
Caretterizzazione alternativa: Automi di Muller
Non approfondiremo (anche questo argomento
potrebbe essere argomento di un seminario)
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
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.
Una stringa temporizzata puo’ essere vista come input
di un automa. Il simbolo si e’ letto al tempo ti.
Un linguaggio temporizzato su S e’ un insieme di
stringhe temporizzate su S.
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.
Alla tabella e’ associato un insieme di orologi (variabili
a valori reali)
Gli orologi avanzano tutti contemporaneamente
Un orologio puo’ essere azzerato da una transizione.
In qualsiasi istante il valore di un orologio da’ il tempo
passato dal suo ultimo azzeramento.
Automi temporizzati (1)
Ogni transizione puo’ avere un vincolo sul valore degli
orologi.
Lo stato successivo dipende non solo dal simbolo letto,
ma anche dal tempo del simbolo letto rispetto ai tempi
dei simboli precedenti.
Automi temporizzati (2)
s0
a, x:=0
s1
b, (x<2)?
L1={((ab)w,t)| per ogni i, t2i<t2i-1 + 2}
Il ritardo tra ogni a e il b successivo e’ al massimo 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) }
Il clock x misura il ritardo tra a e il c successivo (< 1)
Il clock y misura il ritardo tra b e il d successivo (> 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:
a e’ il simbolo di input
lC e’ l’insieme di orologi che la transizione azzera
d e’ il vincolo temporale
Linguaggio Accettato
Un automa temporizzato e’ dato da una tabella
temporizzata e da un insieme FS di stati di
accettazione.
Per definire il linguaggio accettato dobbiamo
estendere il concetto di computazione, run
Le stringhe temporizzate accettate saranno quelle che
contengono almeno uno stato di F infinite volte
Computazioni
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.
Un run e’ una sequenza infinita di stati estesi, in cui ad ogni mossa
viene letto un simbolo, e viene fatto avanzare il tempo in modo
conforme ai vincoli temporali
Inizialmente, l’automa si trova in uno dei suoi stati iniziali e i
valori dei clocks sono tutti zero
Run
Data una tabella temporizzata <S,S,S0,C,E>, un run r su una
stringa temporizzata (s,t) e’ una sequenza infinita di stati estesi,
<s_0,n_0>, <s_1,n_1>, <s_2,n_2>,…..
dove
•n_0(x)=0 per ogni orologio x e s_0  S0
• per ogni i>=1 esiste <s_i-1,s_i, s _i,l,d>  E dove
1) n _i -1 + (t _i - t _i -1) soddisfa d
2) n _i = [Y0] n _i -1 + (t _i - t _i -1) per ogni clock Y di l
Linguaggio Accettato
Un run r su una stringa temporizzata (s,t) e’
accettante sse inf(r)F.
Il linguaggio accettato e’ quello delle stringhe
temporizzate che hanno almeno un run accettante
Un linguaggio temporizzato e’ regolare se esiste un
automa di Büchi temporizzato che lo accetta.
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.
Automi temporizzati (17)
Sono state studiate varie proprieta’ (classici problemi di
decisione) dei TA
Alcuni problemi sono decibili (esistono algoritmi effettivi), altri
problemi sono indecidibili
In generale gli stati estesi sono infiniti!
Presenteremo un algoritmo (un risultato importante) che
permette di verificare se il linguaggio accettato da un automa
temporizzato e’ vuoto:
esiste almeno una stringa temporizzata in L(A) ?
Automi temporizzati (17)
Idea: costruire un automa di Buchi (senza tempo) a stati finiti
che accetta tutte e sole le stringhe di Untime(L(A))
Ricordiamo che Untime(L(A)) sono le stringhe s  Sw tali che
per (s,t) L(A)
E’ evidente che esiste una stringa s  Untime(L(A)) sse esiste
una sequenza temporizzata t tale che (s,t) L(A)
Non e’ possibile buttare via il tempo ed i vincoli di tempo
perche’ Untime(L(A)) dipende dal tempo
Infatti i vincoli temporali sulle transizioni influenzano le mosse
possibili in un certo stato
Automa delle Regioni
In generale gli stati estesi sono infiniti, ma si possono
raggruppare in un numero finito di insiemi con le stesse
proprieta’.
In particolare, gli stati estesi possono essere partizionati in
classi di equivalenza, che mettono insieme le interpretazioni
che sono simili
Automa delle Regioni
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.
Li possiamo identificare
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
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, s,[n]> .
Lo stato s,[n]> simula tutti gli stati estesi <s,n> di A
per ogni interpretazione n
Automa delle Regioni
Proprieta’ importanti delle clock regions:
•
•
Le clock regions sono finite (gli stati sono finiti)
Ogni interpretazione all’interno di una classe di equivalenza
soddisfa esattamente gli stessi vincoli
le interpretazioni nella classe soddisfano gli stessi vincoli
(possono eseguire la stessa transizione, ma con tempi diversi)!!!
Rimane da capire come definire le mosse dell’automa delle regioni
Successore Temporale
•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’.
•Data la forma dei clocks e la definizione di equivalenza tra
interpretazioni esiste un semplice algoritmo per determinare
tutti e soli i successori temporali di una clock region
•Facciamo vedere un esempio
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 (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.
La costruzione e’ comunque alla base di altri algoritmi per TA,
anche per la verifica di sistemi