Home

Federica EU

1/12

Adriano Peron » 16.Proprietà degli Automi Temporizzati

Temi della lezione

Linguaggi temporizzati

Definizioni
Confronto con i linguaggi di Buchi

Proprietà degli automi temporizzati

Proprietà di chiusura dei linguaggi temporizzati.
Determinizzazione
Espressività in presenza di transizioni interne.

Comportamenti e sequenze temporizzate

Un comportamento infinito nell’LTS a partire da uno stato iniziale

$s_0 \stackrel{h_0}{\longrightarrow}s_1\stackrel{h_1}{\longrightarrow}s_2 \ldots$

Un comportamento è accettante se attraversa un numero infinito di stati di successo (stati costruiti su locazioni finali dell’automa).

Tale comportamento induce una sequenza temporizzata

$\alpha =(\alpha_1,\alpha_2)$
costruita come segue:

$\alpha_1(i) = h_j$ per qualche $j \geq 0 \mbox { e } h_j$ è l’i-esimo simbolo dell’alfabeto $\Sigma\setminus \{\tau\}$ che occore nel prefisso iniziale di lunghezza j+1 del comportamento.
$\alpha_2(i) = \sum \{t_i : h_i=\tau(t_i), i < j \}$
Si osservi che le eventuali azioni interne non vengono considerate per costruire la funzione $\alpha_1$

Linguaggio accettato da un automa temporizzato

Esempio:

$s_0 \stackrel{\tau(1)}{\longrightarrow}s_1\stackrel{\tau(0,5)}{\longrightarrow}s_2\stackrel{a}{\longrightarrow}s_3\stackrel{\tau}{\longrightarrow}s_4\stackrel{\tau(0,3)}{\longrightarrow}s_5\stackrel{b}\longrightarrow}s_6\ldots$

La sequenza temporale indotta dal comportamento è
$\alpha_1(0)=a\;\;\; \;\;\;\;\; \alpha_1(1)=b\;\;\;\;\;\;\;\; \alpha_1(2)=\ldots$

$\alpha_2(0)=1,5\;\;\;\;\; \alpha_2(1)=1,8\;\;\;\;\; \alpha_2(2)=\ldots$

Una sequenza temporizzata $\alpha$ è accettata da un un automa TA se

rispetta la proprietà di progresso ed
è indotta da un comportamento accettante dell’LTS dell’automa.

Il linguaggio accettato da un automa è l’insieme delle sequenze temporizzate accettate dall’automa.

Esempio di linguaggio accettato da automa temporizzato

L’automa temporizzato in figura accetta sequenze temporizzate $\alpha = (\alpha_1, \alpha_2)$ che hanno la seguente forma

$\alpha_1(2i) = a\;\;\;\;\;\;\;\;\; \;\;\;\;\;\;\;\;\; &\mbox{ per } i\geq 0\\$

$\alpha_1(2i+1) = b\;\;\;\;\;\;\;\;\;\;\;\; &\mbox{ per } i\geq 0\\$

$\Delta_i \leq 1 \;\;\; \;\;\; \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; & \mbox{ per } i\geq 0$

$\Delta_{i+1} < \Delta_i & \mbox{ per } i\geq 0$

Con $\Delta_i = \alpha_2(2i+1)-\alpha_2(2i)$

Fig.1 Esempio di automa e linguaggio temporizzato.

Linguaggi non temporizzati e temporizzati

La classe dei linguaggi accettati da automi temporizzati e quella accettata dagli automi di i Büchi non sono direttamente confrontabili:

Automa di Büchi: un linguaggio è un insieme di parole di lunghezza infinita.

Automa Temporizzato: un linguaggio è un insieme di sequenze temporali.

E’ possibile confrontare una parola di lunghezza infinita con una sequenza temporale
$\alpha = (\alpha_1, \alpha_2)$ rimuovendo l’informazione temporale, cioè considerando la sola componente $\alpha_1$ che può essere letta come una parola.

$untimed(\alpha)=\alpha_1(0).\alpha_1(1).\alpha_1(2). \ldots$

Per ogni linguaggio L accettato da un automa temporizzato il linguaggio

$untimed(L) = \{untimed(\alpha) : \alpha \in L \}$

è un linguaggio accettato da un automa di Büchi.
La proiezione non temporizzata dei comportamenti di un automa temporizzato è dunque riconducibile ai comportamenti di un semplice automa di Büchi.

Proprietà di chiusura degli automi temporizzati

La classe dei linguaggi accettati da automi temporizzati soddisfa le seguenti proprietà di chiusura rispetto operazioni insiemistiche

E’ chiusa rispetto all’operazione di unione di due linguaggi di sequenze temporizzate L’ e L”.

E’ facile costruire un automa non deterministico che come mossa iniziale decida di simulare il comportamento di un automa che accetti L’ oppure di un automa che accetti L” (e prosegua il comportamento coerentemente con la scelta fatta)

E’ chiusa rispetto all’operazione di intersezione di due linguaggi di sequenze temporizzate L’ e L”.

Dati due automi temporizzati che accettano L’ e L” lla costruzione dell’automa temporizzato che accetta la loro intersezione è del tutto simile a quella già incontrata per l’analogo problema negli automi di Büchi.

Non è chiusa rispetto all’operazione di complemento.

Si ricorda che gli automi di Büchi deterministici non sono chiusi rispetto al complemento ma gli automi non-derministici di Büchi lo sono.

Automi temporizzati: complementazione

Esempio di linguaggio di sequenze temporizzate non-complementabile.

L’automa temporizzato in figura accetta sequenze temporizzate $\alpha = (\alpha_1, \alpha_2)$
che hanno la seguente forma
$\begin{array}{ll}\alpha_1(i) = a &\mbox{ per } i\geq 0\\\alpha_2 (j)-\alpha (i) = 1 &\mbox{ per qualche } 0\leq i < j\end{array}$

Si può dimostrare che non esiste nessun automa temporizzato che possa riconoscere il linguaggio di sequenze temporizzate complementare in cui non capita che due arbitrarie coppie di a siano comunicate a distanza di tempo unitaria.

Fig.2 Automa che accetta un linguaggio non complemetabile.

Automi temporizzati: determinizzazione

Preliminare è la comprensione della nozione di determinismo negli automi temporizzati.

Per gli automi di Büchi il trigger deve essere esclusivo:
Per coppie di transizioni $\langle q_1,a,q_2\rangle, \langle q_1,a',q'_2\rangle$ se $a=a' \mbox{ allora } q_2=q'_2$

Per gli automi temporizzati si considera trigger e condizione temporale.

Un automa temporizzato

$TA = \langle\Sigma ,Loc, Loc_{0}, C, \delta ,Inv, F \rangle$ ,
è deterministico se per ogni coppia di transizioni uscenti dalla stessa locazione

$\langle l_1,a,\phi,Y,l_2\rangle, \langle l_1,a',\phi',Y',l'_2\rangle$

Se $a=a' \mbox{ allora } \phi_1 \wedge \phi_2 \equiv False$ .

Fig.3 Determinismo e Non-determinismo.

Determinizzazione di automi temporizzati

Gli automi temporizzati condividono con gli automi di Büchi la proprietà di non essere determinizzabili.

L’automa temporizzato in figura è non-deterministico (stesso esempio della mancata chiusura per complemento).

Il controllo sul tempo trascorso tra due interazioni arbitrariamente distanti può essere fatto solo usando il non-determinismo.

Non esiste un automa temporizzato deterministico in grado di accettare il linguaggio di sequenze temporizzate

$\alpha=(\alpha_1,\alpha_2)\;\text{con}$

$\alpha_1 (i)=0\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\text{per}\; i\geq 0$

$\alpha_2 (j)-\alpha (i)=1\;\;\;\ \text {per qualche}\; 0\leq i <j$

Fig.4 Automa non determinizzabile.

Automi temporizzati e transizioni interne

Le transizioni interne o $\tau$ transizioni permettono di avere transizioni di controllo che non sono determinate dall’occorrenza di un trigger.

Negli automi temporizzati il tempo di scatto di una $\tau$ -transizione.
Non è influenzato dal tempo di trasmissione di un trigger.
Può essere influenzato solo dall’invariante associato alla locazione.

Permettere l’uso di $\tau$ transizioni negli automi di Büchi permette maggiore facilità e naturalezza descrittiva ma non aumenta il poter espressivo.

La classe dei linguaggi accettati da automi di Büchi con o senza transizioni interne è la stessa.

Permettere l’uso di $\tau$ -transizioni negli automi temporizzati.
Accresce facilità e naturalezza descrittiva.
Aumenta il poter espressivo degli automi temporizzati

La classe dei linguaggi accettati da automi temporizzati con transizioni interne include propriamente quella dei linguaggi accettati senza transizioni interne.

Esempio di espressività di automi temporizzati con azioni interne

L’automa in figura accetta solo sequenze di simboli a trasmessi solo a tempi interi.
Più precisamente accetta il linguaggio di sequenze temporizzate

$\alpha=(\alpha_1,\alpha_2)\;\text{con}$

$\alpha_1 (i)=a\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\text{per}\; i\geq 0$

$\alpha_2 (i)\in \mathbb{N} \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\text{per}\; i\geq 0$

L’uso delle transizioni interne serve a scandire passi unitari discreti.
Senza transizioni interne non è possibile fare tutti i passi discreti necessari perché non è garantito che per ogni passo discreto necessario vi sia una interazione a quel tempo.

Il linguaggio non è accettabile da un automa temporizzato senza transizioni interne.