Home

Federica EU

1/18

Adriano Peron » 15.Specifica di sistemi real time: Automi Temporizzati

Temi della lezione

Introduzione alla specifica di sistemi con proprietà temporali critiche.

Il formalismo degli automi temporizzati (Timed Automata):

sintassi;
linguaggi di tracce temporizzate;
esempi di linguaggi;
semantica;
proprietà dei linguaggi di tracce temporizzate.

Sistemi con propretietà temporali critiche

La correttezza dei comportamenti in sistemi temporalmente critici (Time Critical) non dipende solo dalla forma e dai valori delle interazione con l’ambiente che avvengono nella computazione ma anche dai precisi istanti temporali in cui interazioni e scambi di valori avvengono.

Non basta il solo ordinamento delle transizioni/azioni o più in generale l’informazione causale tra le transizioni/azioni;
L’informazione temporale legata ad ogni transizione/azione in un comportamento non può essere trascurata (astratta).

Esempi di vincolo temporizzati per sistemi time critical

Le sbarre del casello ferroviario devono abbassarsi almeno un minuto prima del passaggio del treno
L’esposizione alle radiazioni in un macchinario di medicina nucleare non può superare tre secondi.
Il tempo tra la rilevazione di parametri anomali da parte dei sensori e l’attivazione di procedure di sicurezza non può eccedere un decimo di secondo.

I formalismi di specifica fin ora considerati:

non permettono di esprimere vincoli sui comportamenti in modo quantitativo;
permettono solo di esprimere in vincoli in modo qualitativo (ordinamento di transizioni/azioni).

Automi temporizzati

Gli automi temporizzati (Timed Automata) sono una estensione degli automi di Büchi.

Come gli automi di Büchi, i Timed Automata intrattengono un rapporto continuativo con l’ambiente (comportamento infinito)

I Timed Automata sono diagrammi stato-transizione decorati con vincoli temporali.

A differenza degli automi di Büchi ad ogni passo di reazione la scelta del prossimo stato non dipende solo dallo stato corrente e dallo stimolo fornito dall’ambiente ma può anche dipendere dai tempi in cui lo stimolo corrente e quelli
precedenti sono occorsi.

L’informazione temporale (avanzamento del tempo) è associata ad orologi (Clock) che registrano l’avanzare del tempo.

Operazioni sugli orologi:

lettura del valore temporale corrente e confronto con costanti temporali;
azzeramento dell’orologio.

Ad ogni istante, il valore temporale segnato da un orologio è pari al tempo trascorso dal suo ultimo azzeramento.

Automi temporizzati

Un clock è una variabile interpretata su un dominio numerico positivo denso:

Razionali positivi (oppure)
Reali positivi.

Con riferimento alla struttura di una transizione:

Trigger è un simbolo dell’alfabeto;
Condizione è una condizione booleana sui Clock;
Azione è un insieme di orologi da azzerare.

Una transizione può scattare quando il trigger viene recepito e la condizione temporale è soddisfatta.
Allo scatto della transizione gli orologi indicati vengono azzerati.

Fig.1 Struttura transizione.

Automi temporizzati: Sintassi vincoli temporali

Per esprimere costanti temporali si assume di adottare il dominio temporale dei razionali positivi ${\cal Q}^{\geq 0}$ .

Dato un insieme di orologi C, l’insieme dei vincoli $\Phi(C)$ ,
è formato secondo la seguente sintassi

$\phi ::= True\ \mid\ x < c\ \mid\ x \leq c\ \mid\ x > c\ \mid\ x \geq c\ \mid\ \phi \wedge \phi$

con $c \in {\cal Q}^{\geq 0} \mbox{ e } x \in C$ .

Nella definizione:

la condizione True rappresenta l’assenza di un vincolo temporale;
è possibile solo confrontare un orologio con una costante temporale.

Sono possibili definizioni alternative che prevedono

uso libero dei connettivi booleani $\wedge , \vee , \neg$ ;
confronti tra orologi (detti vincoli diagonali, ad es $x < y$ ).

Automi temporizzati: sintassi

Sintatticamente gli automi temporizzati sono una estensione degli automi di Büchi.

Un Automa Temporizzato è una tupla

$TA = \langle\Sigma ,Loc, Loc_{0}, C, \delta ,Inv, F \rangle$ , dove

$\Sigma$ è l’alfabeto di input;
Loc è l’insieme finito delle locazioni (gli stati di un automa di Büchi);
$Loc_{0}$ è la locazione iniziale;
C è l’insieme degli orologi;
$\delta \subseteq Loc \times \Sigma \times \Phi(C) \times<br /> 2^{C} \times Loc$ è la relazione di transizione;
$Inv : Loc \longrightarrow \Phi(C)$ è la funzione di invarianza;
$F \subseteq Loc$ è l’insieme delle locazioni finali.

La relazione di transizione descrive transizioni decorate da una tripla che comprende un simbolo di trigger, un vincolo temporale e un insieme di orologi da azzerare.
La funzione di invarianza associa un vicolo ad ogni locazione, vincolo che deve essere soddisfatto per poter permanere nella locazione associata.
La condizione di accettazione è uguale a quella degli automi di Büchi.

Sequenze temporizzate

Il flusso delle interazioni tra ambiente e automa è descritto nel caso degli automi da sequenze temporizzate.

Una sequenza temporizzata $\alpha$ è una $\omega$ sequenza di coppie

$(a_0,t_0)(a_1,t_1)(a_2,t_2) \ldots$

$a_0,a_1,a_2, \ldots$ una sequenza infinita di simboli in $\Sigma$ che descrive la sequenza di interazioni.

$t_0,t_1,t_2, \ldots$ una sequenza infinita di valori del dominio temporale che fornisce i tempi delle interazioni.

Alternativamente, si può vedere una sequenza temporizzata come una coppia di funzioni $\alpha=(\alpha_1,\alpha_2)$ :

$\alpha_1:\bbbn \rightarrow \Sigma$ (trigger per ogni interazione);
$\alpha_2:\bbbn \rightarrow {\cal Q}^{\geq 0}$ (tempo per ogni interazione).

Esempio di automa e sequenza temporizzata

Esempio di automa temporizzato su un orologio x.

Le locazioni hanno invariante True (assenza di vincolo)
Le transizioni con trigger b e c azzerano l’orologio

La sequenza temporizzata è compatibile con due cicli iniziali che attraversano la locazione $l_2$ ed un terzo ciclo che attraversa la locazione $l_1$ .

Fig.2 Automa e sequenza temporizzata.

Tempo di scatto di una transizione.

Negli automi temporizzati il tempo di scatto di una transizione controllata da trigger è determinato dal tempo di trasmissione del trigger.

Se non vi sono transizioni interne, le uniche evoluzioni possibili (a parte lo scorrere del tempo), sono determinate dai trigger e dai loro tempi.

Viceversa, la risposta ad un trigger è obbligatoria. Un comportamento che non sia in grado di rispondere ad un trigger (eseguendo una transizione) al tempo di diffusione del trigger è escluso dai comportamenti di successo dell’automa (determina il blocco dell’automa e i comportamenti di successo sono infiniti).

Le transizioni interne o $\tau$ -transizioni, eventualmente presenti, permettono di avere transizioni di controllo che possono avvenire in assenza di trigger esterni.

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.

Invarianti e transizioni interne

Gli invarianti di stato sono l’unico strumento per forzare l’evoluzione di un automa temporizzato in assenza di trigger esterni.

In Figura, la transizione t potrebbe essere preferita alla transizione t’ perché la sua condizione temporale è soddisfatta prima.
Non è possibile forzare questa forma di urgenza.
Non è possibile neppure forzare l’esecuzione di almeno una delle due transizioni al tempo dovuto.

La transizione t” è invece forzata a scattare al più tardi quando l’orologio segna il tempo 3 (per tempi superiori l’invariante non è soddisfatto e non si può permanere nello stato sorgente).
Lo scatto avverrà necessariamente in un tempo che soddisfi $2 \leq x \leq 3$ .
All’interno dell’intervallo la scelta è non-deterministica.

Fig.3 Invarianti.

Sequenze temporizzate: proprietà

Le sequenze temporizzate sono significative per la descrizione del comportamento di un sistema solo se soddisfano due proprietà:

Monotonia:
per ogni $i \geq 0,\ \alpha_2(i+1)\geq \alpha_2(i)$ ;
Progresso:
per ogni $i \geq 0,\mbox{ esiste j tale che }\alpha_2(j) \geq i$ .

Monotonia: impone compatibilità tra ordinamento dei trogger nella sequenza e ordine temporale.
Si osservi che la monotonicità consente che due o più interazioni con l’ambiente avvengano nel medesimo istante temporale.

Progresso: impedisce che vi sia un numero infinito di interazioni con l’ambiente concentrate in un intervallo finito di tempo.

Preliminari alla definizione della semantica

Soddisfacimento di un vincolo temporale.

Una funzione di valutazione degli orologi è una funzione

$v : C \longrightarrow {\cal Q^{\geq 0}}$

che associa un valore temporale ad ogni orologio (il tempo passato dall’ultimo azzeramento).

Val(C) indica l’insieme di tutte le possibili valutazioni degli orologi in C
Si osservi che l’insieme Val(C) ha cardinalità infinita.

Data una valutazione degli orologi v, un vincolo temporale $\phi$ è soddisfatto se $v \models \phi$ , dove
$v\models True$

$v\models x<c\;\;\;\;\;\;\text{se}\;v(x)<c$

$v\models x\leq c\;\;\;\;\;\;\text{se}\;v(x)\leq c$

$v\models x>c\;\;\;\;\;\;\text{se}\;v(x)>c$

$v\models x\geq c\;\;\;\;\;\;\text{se}\;v(x)\geq c$
$v\models \phi_1\wedge\phi_2\;\;\;\text{se}\;v\models \phi_1\;\text{e}\; v\models \phi_2$

Preliminari alla definizione della semantica (segue)

Aggiornamento di una valutazione per avanzamento temporale

Data una valutazione v, l’avanzamento temporale uniforme degli orologi per un quantitativo di tempo t è dato dalla valutazione v+t dove

$v+t(x) = v(x)+t \mbox{ per ogni } x \in C$

Aggiornamento di una valutazione per azzeramento degli orologi
Data una valutazione v e un insieme di orologi Y contenuto in C, l’azzeramento temporale degli orologi in Y (reset) è dato dalla valutazione v-Y, dove
$v-Y(x)=\left\{\begin{array}{ll} 0\;\;\;\;\;\;\; \text{se}\; x\in Y,\\ \\ v(x)\; \text{se}\;\; x\in C\setminus T\end{array}\right$

Semantica degli automi temporizzati

Sia $TA = \langle\Sigma ,Loc, Loc_{0}, C, \delta ,Inv, F \rangle$ un automa temporizzato.

La semantica degli automi temporizzati viene data definendo un LTS

$\langle S_0, S, \Delta \rangle$

Lo stato raccoglie informazioni sul controllo e sulla valutazione corrente degli orologi.

$S \subseteq Loc \times Val(C)$

Gli stati iniziali hanno valutazione dei clock a tempo zero.

$S_0 = Loc_0 \times \{v_0\}$

con $v_0(x)=0 \mbox{ per ogni } x \in C$

Semantica degli automi temporizzati (segue)

Due tipi di transizioni nell’LTS

(1) Il tempo avanza di un quantità t (avanzamento temporale).

L’automa non cambia locazione.
L’avanzare del tempo non deve violare l’invariante della locazione corrente.
Tutti gli orologi avanzano della medesima quantità di tempo t.

(2) L’automa cambia locazione (avanzamento controllo).

Il tempo è bloccato (non avanza).
La nuova locazione raggiunta deve soddisfare l’invariante temporale

Alfabeto delle transizioni dell’LTS

$\Sigma_{\tau}=\Sigma \cup \{\tau(t): t \in {\cal Q}^{\geq 0}\}$

$\{\tau(t): t \in {\cal Q}^{\geq 0}\}$ per avanzamento temporale.
$\Sigma$ per avanzamento del controllo.

Semantica degli automi temporizzati (segue)

L’LTS $\langle S_0, S, \Delta \rangle$ per l’automa
$TA = \langle\Sigma ,Loc, Loc_{0}, C, \delta ,Inv, F \rangle$ ha relazione di transizione

$\Delta \subseteq S \times \Sigma_{\tau}\times S$

L’insieme di transizioni è l’unione dei due seguenti insiemi di transizioni

(1) Il tempo avanza di un quantità t:

$\{\langle(l,v),\tau(t),(l,v+t) \rangle : t\in {\cal Q}^{\geq 0}, (l,v) \in S, v+t \models Inv(l)\}$

(2) L’automa cambia locazione

$\{\langle(l,v),a,(l',v-Y):\left\begin{array}{llll}\langle l,a,\phi,Y, l'\rangle\in \delta,\\ (l,v)\in S, \\ v\models\phi, \\ v-Y\models Inv(l')\}\end{array}\right$

LTS temporizzato

Anche se il numero di locazioni dell’automa è finito, l’LTS della sua semantica ha

numero infinito di stati (infinite sono le valutazioni);
numero infinito di transizioni (infiniti i modi di far avanzare il tempo in un dominio denso).

L’LTS definito è un LTS temporizzato che soddisfa la proprietà espressa in figura.
Se esite un avanzamento temporale t e t=t’+t” allora esiste anche un avanzamento t’ a cui fa seguito un avanzamento t”

Fig.4 Proprietà LTS temporizzato.

Esempio di automa

Esempio di automa temporizzato che permette di esprimere caratteristiche legate alla densità del dominio temporale.

In generale:
In un intervallo finito di tempo possono verificarsi un numero finito ma arbitrariamente grande di interazioni con l’ambiente
la distanza di due interazioni successive può essere arbitrariamente piccola.

Nell’automa in figura i comportamenti accettati sono quelli in cui la sequenza delle differenze temporali tra una occorrenza di a e l’occorrenza successiva di b è strettamente decrescente.