Automi temporizzati

-linguaggi e -automi (1)

Un -linguaggio su un alfabeto finito e’ un sottoinsieme di , l’insieme di tutte le stringhe infinite su .

Una tabella di transizione A e’ una quadrupla <,S,S0,E> dove alfabeto di inputS insieme finito di statiS0S insieme di stati inizialiE SS insieme di archi

-linguaggi e -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 = 1 2 3 … su

r = s0 s1 s2 …

e’ un run di A su purche’ s0S0 e <si-1,si,i>E per i1.

321

-linguaggi e -automi (3)

Per un run, l’insieme

inf(r) consiste degli stati sS tali che s=si per un numero infinito di i0.

Automi di Büchi (1)

Un automa di Büchi e’ una tabella di transizione <,S,S0,E> con un insieme addizionale FS di stati di accettazione.

Un run di A su una stringa 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 tali che A ha un run di accettazione leggendo . s0

s1

a,b

a

a

L’automa accetta tutte le stringhe su {a,b} con un numero finito di b.

Un -linguaggio e’ regolare se e’ accettato da un automa di Büchi.

Automi di Büchi (3)

L1 dopo una occorrenza di a ci sono occorrenze di b

s0s1

b,c

a

a,cb

– L1s0

s1

a,b,c

a

a,c

Automi di Büchi (4)

tra due occorrenze di a, c’e’ un numero pari di occorrenze di b e c (anche zero)

s0s1

b,c

a

ab, c

b, c s2

Automi di Büchi (5)

TeoremaSe L da A e’ riconoscibile da un automa A (regolare) allora lo e’ anche –L. Inoltre e’ possibile costruire l’automa per –L.

TeoremaLa classe degli -linguaggi regolari e’ chiusa sotto le operazioni booleane.

Automi di Büchi (6)

TeoremaE’ decidibile se il linguaggio riconosciuto da un automa di Büchi e’ vuoto.

TeoremaE’ decidibile l’inclusione tra due -linguaggi regolari L1 e L2.Dimostrazione Basta dimostrare che e’ vuota l’intersezione L1w-L2.

Automi di Büchi (7)

Un automa di Büchi A=<,S,S0,E> e’ deterministico se e solo se - c’e’ un singolo stato iniziale (|S0|=1),- il numero di archi etichettati da , uscenti dallo stato s, e’ al piu’ uno per tutti gli stati sS e tutti i simboli .

La classe dei linguaggi riconosciuti dagli automi deterministici e’ strettamente contenuta in quella degli -linguaggi regolari.

Automi di Büchi (8)

s0s1

a,b

a

a

Non c’e’ nessun automa deterministico che riconosce

(a+b)*a

Automi di Muller (1)

Un automa di Muller A e’ una tabella di transizione <,S,S0,E> con una famiglia di insiemi di stati di accettazione, (S).

Un run di A su una stringa 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)

= {{s1}}

Automa di Muller deterministico che riconosce (a+b)*a

TeoremaLa 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.

s0s1

b

a

ab

Linguaggi temporizzati (1)

Modello del tempo: numeri reali non negativi, R.

Una sequenza temporale = 1 2 3 … e’ una sequenza

infinita di valori iR che soddisfa:

1. monotonicita’: 1 2 , i1.

2. progresso: per ogni R c’e’ un i1 tale che i

.

Linguaggi temporizzati (2)

Una stringa temporizzata su e’ (,) dove = 1 2 3 … e’ una stringa infinita su e e’ una sequenza temporale.

Un linguaggio temporizzato su e’ un insieme di stringhe temporizzate su .

Una stringa temporizzata puo’ essere vista come input ad un automa. Il simbolo i e’ presentato al tempo i.

Linguaggi temporizzati (3)

Il LinguaggioL1={(,)| per ogni i, (i5.6)(ia)}su {a,b} e’ il linguaggio delle stringhe temporizzate in cui non ci sono b dopo il tempo 5.6.

Il LinguaggioL1={((ab),)| per ogni i, (2i2i-1) (2i+22i+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 , Untime(L) e’ l’-linguaggio composto dalle stringhe tali che per (,L per qualche sequenza temporale .

Esempio

Untime(L1)=(a+b)*a

Untime(L2)=(ab)

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)

s0s1a, x:=0

a, (x<2)?

L1={((ab),)| per ogni i, 2i2i-1 }

Automi temporizzati (3)

s0s1

a, x:=0 c, (x<1)?

L1={((abcd),)| per ogni i, (4j+34j+1 )e (4j+44j+2

)}

s2 s3

b, y:=0

d, (y>2)?

Automi temporizzati (4)

Dato un insieme di orologi X, l’insieme (X) di vincoli sugli orologi e’ definito induttivamente come

= xc | cx | | 1 2

c costante intera

Un’interpretazione per un insieme di orologi X e’ una funzione da X a R, X R.

Una interpretazione per X soddisfa un vincolo se e solo se e’ valutato a “vero” per i valori dati da .

Automi temporizzati (5)

Per R, denota l’interpretazione che assegna a x il valore (x) .

Per YX, [Y]n denota l’interpretazione che assegna a ciascun orologio yY e assegna (z) a tutti gli orologi zY.

Automi temporizzati (6)

Una tabella di transizione temporizzata A e’ data da una quintupla <,S,S0,C,E>, dove

alfabeto di inputS insieme finito di statiS0S insieme di stati inizialiC insieme di orologiE SS(C)(C) insieme di archi

Una transizione e’ <s,s’,a,,> dove 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.

s0s1b b, (x<2)

L1={((ab),)| per ogni i esiste ji: 2j2j-1

}

s2 s3

a, {x}

Automi temporizzati (7)

a a, {x}

s0

a,b, x<3

L1={(,)| per ogni i esiste ji: ji e j

a}

a, {x}, x=3

Automi temporizzati (8)

s0s1

a, {x}, x=1a, {x}, x=1

L1={((ab),)| per ogni i: (2i-1i) e (2j 2j-1 2j+2 2i+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.

s2 s3b, {y}

Automi temporizzati (9)

b, {y}, y<1

In un linguaggio temporizzato i simboli possono essere arbitrariamente vicini

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.

TeoremaSia L un linguaggio temporizzato regolare.Per ogni parola , Untime(L) se e solo se

esiste una sequenza tale che iQ per ogni i>1 e (,)L.

Gli automi non distinguono tra R e Q.

Automi temporizzati (11)

TeoremaDato un automa di Büchi temporizzato A= <,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,S0,C,E,F>, e’ indecidibile se il linguaggio accettato da A e’ l’insieme di tutte le stringhe su .TeoremaDati due automi A1 e A2, e’ indecidibile se L(A1)L(A2).CorollarioLa classe dei linguaggi non e’ chiusa per complemento.

Automi temporizzati (12)

Un automa temporizzato di Muller A= <,S,S0,C,E,> e’ una tabella di transizione temporizzata, <,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)

e’ {{s0,s2}}

Ogni parola accettata dell’automa soddisfa:. (a(b+c))* (ac)

2. per ogni i1 (2i-1 2i-2) e’ minore di 2 se il simbolo di indice 2i e’ uguale a c, minore di 5 altrimenti.

s0s1 a, x<5 s2

b, {x}

a, x<2

c, {x}

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,S0,C,E,> un automa di Muller.

Notiamo che L(A)=F L(AF) dove AF= <,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,,> di A, l’automa A’F ha una transizione <<s,0>,<s’,0>,a,,>. In aggiunta, se s’ F anche <<s,0>,<s’,1>,a,,>.

Per ogni transizione <s,s’,a,,> di A con s,s’ F, per ogni 1ik l’automa A’F ha una transizione <<s,i>,<s’,j>,a,,> 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)

e’ {{s1,s2}}s1s0 a, x<5 s2

b, {x}

a, x<2

c, {x}

<s0,0> a, x<5

b, {x}

a, x<2

c, {x}

<s1,0><s2,0>

<s1,1>

<s2,2>

a, x<5

a, x<2

c, {x}<s2,1>

c, {x}

a, x<2

c, {x}

Automi temporizzati (17)

Data una tabella temporizzata <,S,S0,C,E>, uno stato esteso e’ dato da una coppia <s,>, dove sS e 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 tR, fract(t) denota la parte frazionaria e t la parte intera. t = t +fract(t)

Automa delle regioni (1)

Sia A=<,S,S0,C,E> una tabella temporizzata. Per ogni xC sia cx la piu’ grande costante tale che xcx o xcx occorre in E.La relazione di equivalenza e’ definita sull’insieme delle interpretazioni per C: ’ se e solo se valgono le seguenti condizioni:

1. per tutti gli xC (x) e ’(x) hanno lo stesso valore oppure (x) e ’(x) sono entrambi maggiori di cx

2. per tutti gli x,yC con (x) cx e (y) cy, fract((x)) fract((y)) se e solo se fract(’(x)) fract(’(y))

3. per tutti gli xC con (x) cx, fract((x)) 0 se e solo se fract(’(x)) 0

Una “clock region” e’ una classe di equivalenza di , denotata []

Automa delle regioni (2)

Si consideri una tabella temporizzata con due orologi, x e y, e cx=2, cy=1.

1

1

0 2

y

x

Regioni

6 vertici (es. [(0,1]))14 segmenti (es. 0xy1) 8 regioni (es 1x2 0y1

fract(x)fract(y))

s1s0a, {y}

s2

s3

b, y=1 c, x<1

c, x=1

a, {y}, y<1

d, x>2

Automa delle regioni (intuizione)

1

1

0 2

y

x

(x)=1.2, (y)=0.9

’ (x)=1.4, ’(y)=0.7

(x)=1, (y)=0.6

’ (x)=1, ’(y)=0.4

(x)=1.5, (y)=2.2

’ (x)=1.5, ’(y)=1.9

Automa delle regioni (3)

Dato A=<,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,>, (A) si trova nello stato ,s,[]>.

Una regione ’ e’ un successore temporale della regione se e solo se per ogni , esiste un tR, positivo, tale che +t’.

Automa delle regioni (4)

Costruiamo i successore temporali di una regione .

Ricordiamo che una regione e’ definita da:

1. per ogni orologio un vincolo xc, c-1xc oppure xcx.2. per ogni coppia x e y tale che c-1xc e d-1yd

compaiono in 1. l’ordine tra fract(x) e fract(y).

linea dei successori temporali

1

1

0 2

y

x

Automa delle regioni (5)

Prendiamo l’insieme C0 dei clock x tali che soddisfa il vincolo xc, con ccx. Supponiamo C0 non vuoto. La prima regione successore, , di e’ data da:

1. per xC0, se soddisfa x=cx soddisfa x>cx altrimenti se soddisfa x=c soddisfa c<x<c+1. Per per xC0, il vincolo in e’ uguale a quello di .

2. Le relazioni tra le parti frazionarie rimangono le stesse (per xC0 la parte frazionaria era 0).

1

1

0 2

y

x

Automa delle regioni (6)

Se il caso precedente non si applica, prendiamo l’insieme C0 dei clock x tali che non soddisfa xcx e che hanno la parte frazionaria massima. Cioe’ per tutti gli orologi y tali che non soddisfa xcx, fract(y)fract(x).

1. per xC0, se soddisfa c-1<x<c, soddisfa x=c, Per per xC0, il vincolo in e’ uguale a quello di .

2. Le relazioni tra le parti frazionarie rimangono le stesse.

1

1

0 2

y

x

Automa delle regioni (6)

Dato A=<,S,S0,C,E> il corrispondente automa delle regioni

(A) e’ definito nel modo seguente:

1. Gli stati di (A) sono coppie <s,> dove sS e e’ una regione.

2. Gli stati iniziali sono della forma <s0,[0]> dove s0S0 e 0(x)=0 per tutti gli orologi di C.

. (A) ha un arco <<s,>,<s’,’>,a> se e solo se c’e’ un arco <s,s’,a,,>E e una regione ’’ tale che (1) ’’ e’ un successore temporale di , (2) ’’ soddisfa , e (3) ’=[0]’’.

Automa delle regioni (7)

s1s0a, {y}

s2

s3

b, y=1 c, x<1

c, x<1

a, {y}, y<1

d, x>1

a

aa

a

a

aa

b

b

b

c

d dd

d

dd

d

d

s0

x=y=

0

s1

0=y<x

<1

s1

0=y,

1=x

s1

0=y,

1<x

s2

1=y<

x

s3

0<y<x

<1

s3

0<y<1

<x

s3

1=y<x

s3

1<y, 1<x

Automa delle regioni (8)

Per un automa temporizzato A=<,S,S0,C,E>, il suo automa delle regioni puo’ essere utilizzato per accettare Untime(L(A))

TeoremaDato un automa temporizzato A=<,S,S0,C,E>, esiste un automa di Büchi su che accetta Untime(L(A)).

L’automa delle regioni puo’ essere utilizzato per dimostrare che il linguaggio accettato da un automa temporizzato e’ vuoto.

Corollario

La classe dei linguaggi non e’ chiusa per complemento.

Ancora sugli automi temporizzati

s1s0a, {x}

s3

a, x=1

aa a

L={(a,)| esiste i1: esiste j i: j=i+1}

Automi di Muller deterministici

Un automa temporizzato A=<,S,S0,C,E> di Muller e’ deterministico se e solo se

- ha solo uno stato iniziale |S0|=1

- per tutti gli sS, per tutti i , per ogni coppia di archi della forma <s , _ , a , _ , 1> e <s , _ , a , _ , 2>, e sono mutamente esclusivi (1 2 e’ insoddisfacibile)

Teorema

La classe dei linguaggi accettati da automi deterministici di Muller e’ chiusa per unione, intersezione e complemento.

Ancora sugli automi temporizzati

A||A’ accetta la composizione di stringhe accettate da A e A’ in cui gli eventi comuni avvengono allo stesso tempo

Composizione parallela

s1s0

a, x=1,{x}

b

s1

a

c

s0

L={(a(bc+cb)),)| i-2i}

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’ (1)

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’ (2)

Verifica di proprieta’ (3)

s1s0

approach, {x}

idT

s2

in, x>2

outs3

exit, x<5

TRAIN

Verifica di proprieta’ (4)

s1s0

lower, {y}

idG

s2

down, y<1

raise, {y}s3

up, (y>1) (y<2)

GATEidG

Verifica di proprieta’ (5)

s1s0

approach, {z}

idC

s2

lower, z=1

exit, {z}s3

raise, z<1

CONTROLLER

Verifica di proprieta’ (6)

s0

in, ~down

s2s1

down

Safety: quando in treno e’ nel passaggio a livello, questodeve essere chiuso

up, ~outin

out

in, ~up

up

Verifica di proprieta’ (7)

s0

~down

s1

down, {x}

Liveness: il passaggio a livello non sta chiuso mai per piu’ di dieci minuti

up

up, x<10

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={(,)| per ogni i, i(i,i+1] e (i=i+1 e i=a)

oppure (i(i,i+1) e i=b)}

s0

a, {x}, x=1

s1

b, 0<x<1

, {x}, x=1