Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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.

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.

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.

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.

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.

Fig.5 Automa con azioni interne.

Fig.5 Automa con azioni interne.


Riepilogo della gerarchia espressiva per gli automi temporizzati


  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion