Home

Federica EU

1/15

Adriano Peron » 17.Problemi di decisione negli Automi Temporizzati

Temi della lezione

Proprietà di decisione negli automi temporizzati

Decisione della proprietà del linguaggio vuoto
Tecnica di regionalizzazione
Automa delle regioni
Complessità del problema del vuoto
Raggiungibilità

Problema di decisione del vuoto

Il problema di decisione del vuoto consiste nello stabilire se un automa temporizzato accetta almeno una sequenza temporizzata.

E’ come visto un problema essenziale per la verifica di sistemi in quanto usato nell’approccio alla verifica mediante teoria degli automi per determinare se esiste almeno una sequenza temporizzata che viola le proprietà desiderate del sistema.

La possibilità di decidere il problema del vuoto e la complessità della decisione sono dunque fattori essenziali nelle attività di verifica e in particolare di model checking.

Situazione nel caso non temporizzato (Automi di Büchi)

L’LTS di un automa di Büchi è finito (numero finito di stati e di transizioni)

Il problema della raggiungibilità di uno stato è un semplice problema di raggiungibilità di un nodo dal nodo iniziale in un grafo (complessità lineare nella taglia dell’LTS).

Il problema del vuoto è un semplice problema di raggiungibilità, in un grafo, di un ciclo contenente almeno uno stato finale (complessità lineare nella taglia dell’LTS).

Problema di decisione del vuoto (vuoto)

Situazione nel caso temporizzato (Automi Temporizzati)

L’LTS di un automa temporizzato definito dalla semantica ha taglia non finita per la presenza di un dominio temporale infinito (denso).

L’ LTS definito dalla semantica presenta un numero infinito di stati.
Ad uno stato è associato ad una delle possibilmente infinite funzioni di valutazione degli orologi.

L’ LTS definito dalla semantica presenta un numero infinito di transizioni.
Anche in presenza di un numero finito di stati il numero di possibili transizioni che regolano l’avanzamento temporale in un dominio denso sono infinite.

Fortunatamente, ai fini della risoluzione del problema del vuoto, l’informazione contenuta nell’LTS è ridondante.

E’ possibile trovare una rappresentazione finita dell’LTS che permetta di risolvere equivalentemente il problema del vuoto.

La tecnica per la astrazione dell’informazione temporale si chiama regionalizzazione.

La rappresentazione dell’LTS equivalente ai (soli) fini della risoluzione del problema del vuoto si chiama Automa delle regioni (di fatto, un automa di Büchi).

Regionalizzazione

Tecnica per l’astrazione dell’informazione temporale (valutazioni degli orologi).

Idea: definire una relazione di equivalenza che metta in relazione una coppia di valutazioni solo quando possano in tutte le occasioni influenzare allo stesso modo l’evoluzione dell’automa temporizzato in considerazione.

Se due valutazioni v e v’ degli orologi sono poste in relazione di equivalenza $v \sim v'$
allora deve essere rispettata la seguente proprietà di correttezza

Per ogni locazione Loc e per ogni transizione t
esiste una transizione mediante t dallo stato (Loc,v)
se solo se
esiste una transizione mediante t dallo stato (Loc,v’)

Il problema diventa ora:

trovare una relazione che soddisfi la proprietà di correttezza;
fissare la relazione in modo che il numero delle classi di equivalenza sia finito;
trovare una rappresentazione simbolica della classe di equivalenza (regione).

Definizione della relazione di equivalenza

Notazione

C insieme di orologi usati nei vincoli temporali di un automa TA e Val(C) insieme delle possibili valutazioni;
$c_x$ massima costante temporale che compare in un vincolo (si assume che si siano usate solo costanti temporali intere positive);
int(t) e frac(t) indicano la parte intera e frazionaria di un valore t del dominio temporale;

La relazione di equivalenza $\sim \subseteq Val(C) \times Val(C)$ è tale per cui $v \sim v'$ se e solo se le tre seguenti condizioni sono soddisfatte

$(1) \mbox{per ogni }x\in C \mbox{ o }int(v(x))=int(v'(x)) \mbox{ oppure } v(x)> c_x \mbox{ e } v'(x) > c_x$

$(2) & \mbox{per ogni }x\in C & \mbox{ se }v(x)\leq c_x \mbox{ allora }<br /> frac(v(x))=0 \mbox{ se e solo se } frac(v'(x))=0 \;\;\;\;\;\;\;\;\;\text{(1)}$

$(3) & \mbox{per ogni }x,y\in C & \mbox{ se }v(x)\leq c_x \mbox{ allora }<br /> frac(v(x)) \leq frac(v(y)) \mbox{ se e solo se } frac(v'(x)) \leq frac(v'(y))$

Una classe di equivalenza indotta dalla reazione di equivalenza è detta regione.

Esempio di regionalizzazione per un automa

Esempio di regionalizzazione (segue)

Regioni puntuali corrispondenti a valutazioni intere (condizioni 1 e 2 di equivalenza)
X=0, y=0
X=0, y=1
X=1, y=0
X=1, y=1
Semirette (condizioni 1 e 2 di equivalenza)
X=0, y > 1
X=1, y > 1
X > 1, y=0
X > 1, y=1

Fig.2 Esempio di regionalizzazione.

Esempio di regionalizzazione (segue)

Segmenti di retta
X = 0, 0 < y < 1
X = 1, 0 < y < 1
0 < x < 1, y = 0
0 < x < 1, y = 1
0 < x < 1, 0 < y < 1, x=y

Aree

X > 1, y > 1
X > 1, 0 < y < 1
0 < x < 1, y > 1
0 < x < 1, 0 < y < 1, x < y
0 < x < 1, 0 < y < 1, x > y

Fig.2 Esempio di regionalizzazione.

Definizione simbolica delle regioni

Come illustrato nell’esempio tutte le regioni possono essere descritte da una opportuna combinazione di disequazioni sui valori degli orologi.

Ogni regione può essere rappresentata scegliendo.

Per ogni orologio x una disequazione dall’insieme

$\{x=c : c=0,1, \ldots, c_x\} \cup \{c-1 < x < c : c=1, \ldots, c_x\} \cup \{x > c_x\}$

Per ogni coppia di orologi x e y se i vincoli scelti sono entrambi della forma
$c-1 < x < c \mbox{ e } d-1 < y < d$ si sceglie uno dei seguenti vincoli.

$\{x=y, x < y, x>y\}$

Visto l’aspetto combinatorio è possibile dare la seguente limitazione superiore al numero di regioni.
$\mid C \mid \cdot 2^{\mid C \mid} \prod_{x \in C}(2c_x + 2)$
Il numero di regioni è finito.
Dipende esponzialmente dal numeo di orologi e dalla costante massima nei vincoli.

Spostamento tra le regioni per avanzamento del tempo.

La nozione di tempo-successore tra le regioni permette di stabilire come ci si sposta tra le regioni quando il tempo avanza.
Una regione R’ è tempo-successore di una regione R (succ(R,R’)) se e solo se per ogni valutazione $v \in R$ esiste un tempo t tale che $v+t \in R'$

Esempio: le regioni tempo-successori di

R(0 < x <1,y=0) sono le regioni toccate dalla semiretta tracciata in figura:

X =
1,0<y<1
0 < x < 1, y = 0
0 < x < 1, 0 < y < 1, x>y
X > 1, y > 1
X > 1, 0 < y < 1 X > 1, y = 1

Fig.3 Relazione tempo-successore

Automa delle regioni

L’insieme delle regioni definito permette di costruire un automa delle regioni per l’automa temporizzato TA.

L’automa delle regioni è un automa di Büchi i cui stati sono coppie.

Una locazione dell’automa TA (parte di controllo).
Una regione che codifica l’informazione temporale astratta sull’esecuzione.

Ciascuna transizione dell’automa delle regioni riassume tre passi fondamentali.

Un avanzamento temporale da una regione R si sceglie una regione successore R” tale che succ(R,R”).
Una transizione di TA che soddisfa i suoi vincoli temporali nella regione R”.
Una operazione di reset degli orologi che modifica la regione R” nella regione R’ da associare alla locazione di destinazione della transizione.

Automa delle regioni (segue)

Sia $TA = \langle\Sigma ,Loc, Loc_{0}, C, \delta ,Inv, F \rangle$ e Reg(TA) l’insieme delle regioni per TA.

L’automa delle regioni è un automa di Büchi $RA(TA)\langle\Sigma ,Q, Q_{0}, \delta' ,F' \rangle$

$Q = L \times Reg(TA)$
$Q_{0} = Loc_{0} \times [v_0]$ (la regione della valutazione iniziale)

$\delta' = \{\langle (l,R),a,(l',R') \rangle : & \langle l, a, \phi, Y, l'\rangle \in \delta$

$\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;& succ(R,R'') \mbox{ per qualche } R'' \in Reg(TA),$

$& R'' \models \phi,$

$& R'' \models Inv(l)\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\text{(2)}$

$& R' \mbox{ la regione ottenuta da R'' azzerando gli orologi in Y}$

$& R' \models Inv(l')$

$\}$

$F' = F \times Reg(TA)$

Decidibilità del vuoto per automi temporizzati

Vale il seguente risultato.

Un automa temporizzato TA accetta il linguaggio vuoto se e solo se il suo automa delle regioni RA(TA) accetta il linguaggio vuoto.

Il problema del vuoto per gli automi temporizzati è decidibile perché il problema del vuoto su un automa di Buchi può essere risolto in tempo lineare.
La complessità dell’algoritmo proposto per il problema del vuoto dipende dalla taglia dell’automa delle regioni.
La taglia dell’automa delle regioni dipende direttamente dal numero delle regioni dell’automa (esponenziale nel numero degli orologi e delle costanti di confronto nelle valutazioni temporali)

La costruzione evidenzia che, nel caso generale, il problema di verificare un sistema temporizzato ha in genere un costo computazionale superiore a quello della verifica di un sistema non temporizzato.

E’ dimostrabile che la complessità del problema del vuoto per Automi temporizzati è PSPACE-completo.

Automa delle regioni per TA di Fig.1

Commenti all’esempio

Nell’esempio sono riportati solo gli stati effettivamente raggiungibili dallo stato iniziale.

Si osservi che nell’esempio l’analisi dell’automa temporizzato porta a predire che il linguaggio accettato non è vuoto: esiste infatti un ciclo che comprende stati di accettazione (comprendenti le locazioni $l_3$ o $l_4$ .

Si osserva che non tutti gli stati hanno archi uscenti.
Ad esempio, dallo stato con regione x>1, y=0 non è possibile trovare alcuna regione successore che soddisfi il vincolo x=1.
Le computazioni che arrivino ad un tale stato non potendo proseguire non potranno essere computazioni accettanti.