Automi temporizzati cooperanti
(TCA)
Automi cooperanti (CA)
Un CA consiste di n automi finiti, ciascuno con insieme di stati,
stato iniziale e tabella delle transizioni.
Gli automi si sincronizzano prendendo le transizioni in accordo
con il simbolo letto, il loro stato interno e formule condizionali
del tipo ”la componente i è correntemente nello stato q”.
Automi temporizzati cooperanti (TCA) (1)
I TCA estendono i CA:
1. consentendo vincoli temporali sulle transizioni
2. Consentendo passi consistenti di sequenze di transizioni
(attività stimolate dall’ambiente ma interne e non urgenti
ossia con consumo di tempo non nullo).
Un ambiente è una tripla a = < a1, a2, a3>
dove: a1: N 2S dà l’insieme dei segnali comunicati a ogni
interazione
a2: N Time dà il tempo a ogni interazione e soddisfa
monotonicità e progresso; Time è un dominio del tempo
denso
a3: N Time dà la durata della comunicazionedurante
l’interazione, ossia a2(i) + a3(i) ≤ a2(i+1)
Automi temporizzati cooperanti (TCA) (2)
La collezione PS delle condizioni ambientali su S è definita
induttivamente come segue:
True, a  S
p1  p2 , p1 p2 , p1 per p1 , p2  PS
Per un insieme di simboli di stato Q la collezione delle condizioni
interne GQ è definita induttivamente come segue:
true, q = t, q[t], q{t} dove t  Time
p1  p2 , p1 p2 , p1 per p1 , p2  GQ
Per consentire passi consistenti di sequenze di transizioni
distinguiamo tra stati di input (che iniziano e terminano
un’attività) e stati non di input (stati intermedi di un’attività
interna.
La condizione di accettazione è una condizione di Buchi.
Automi temporizzati cooperanti (TCA) (3)
Un TCA è una tupla M = <M1,…, Mn, I, F>, dove
ogni automa sequenziale Mi è una tripla <Qi, q0i, di> tale che
Qi è un insieme finito di stati Q1,…, Qn disgiunti, Q =  1≤i≤n Qi
q0i  Qi stato iniziale
di sè la relazione di transizione
l’insieme I degli stati di input è tale che 1≤i≤n {q0i}  I  Q
F  I è l’insieme degli stati accettanti.
Una configurazione locale per un automa sequenziale Mi è
Ci = <qi, ini, outi, si >, dove 1) qi  Q è stato abilitato da Qi
2) ini : Qi  Time funzione di abilitazione dello stato dà il tempo
più recente in cui lo stato è stato abilitato ed è indefinito se non è
stato mai abilitato 3) outi : Qi  Time funzione di disabilitazione
dello stato 4) si  Time tempo locale.
Automi temporizzati cooperanti (TCA) (4)
Una configurazione locale Ci= <qi, ini, outi, si> è di input se qi  I.
Una configurazione locale Ci= <qi, ini, outi, si> è iniziale se qi = q0i
si = 0, ini(q0i) = 0 e ini indefinito altrimenti, outi indefinito per ogni q
(denotata C0i ).
Una configurazione globale C è <C1, … Cn, a, m> dove:
1) Ci configurazione locale
2) a ambiente
3) m  N indica che si tratta della m-esima iterazione, ossia
a = <a1(m),a2(m),a3(m)>.
Automi temporizzati cooperanti (TCA) (5)
Sia C = <C1, … Cn, a, m> con Ci= <qi, ini, outi, si> allora
le condizioni interne True, q[t], q{t}, q = t sono indefinite a s se si>s
q[t] valuta a True al tempo s sse si≤s, q=qi e ini(q)≤ s-t, ossia q è stato
abilitato per un tempo ≤ t
q{t} valuta a True al tempo s sse q=qi oppure s-t ≤ out(qi)≤s, ossia q è
stato disabilitato da al più t
q = t valuta a True se e solo se q è stato abilitato da esattamente t.
La proposizione di ambiente p  P è valutata interpretando a True i
simboli in {true}  {a: a  <a1(m), a2(m) ≤ s ≤ a2(m)+a3(m)}.
Automi temporizzati cooperanti (TCA) (6)
Data una configurazione C = <C1, … Cn, a, m> c’è una derivazione
locale da Ci= <qi, ini, outi, si> a Ci’= <qi’, ini’, outi’, si’> denotata
Ci C Ci’ se:
1) si’  a2(m)
2) <qi, p, g, qi’>  di
3) ini’(qi’) = si’ e ini’(q) = ini(q) per qi ≠ q
4) outi’(qi) = si’ e outi’(q) = outi(q) per qi ≠ q
5) p valuta a True in a al tempo si’ e interazione m
6) g valuta a True in C al tempo si’
La derivazione è urgente se non c’è una derivazione locale Ci C Ci”
al tempo s” con max{si, a2(m)} ≤ s”< si’
Automi temporizzati cooperanti (TCA) (7)
Un passo locale da una configurazione C = <C1, … Cn, a, m> è una
sequenza di derivazioni locali Ci C Ci1  … C Cin C Ci’ denotata
Ci C Ci’ dove Ci e Ci’ sono configurazioni locali di input e Cin non
è una configurazione di input per ogni 1 ≤ j ≤ n.
Il passo è urgente se le configurazioni locali sono urgenti.
Il passo locale Ci C Ci’ è ghost se Ci = Ci’ .
Il comportamento di un TCA è una composizione di passi locali che
garantisce causalità e massimalità. Il passo locale di una componente è
fatto rispetto alle configurazioni locali delle altre componenti che sono
o nelle configurazioni iniziali o nelle configurazioni raggiunte nello
stesso passo purché ne sia data una giustificazione causale.
Un passo è urgente se consiste solo di passi urgenti. Un passo è reattivo
se ciascun passo locale termina prima della successiva interazione con
l’ambiente.
Automi temporizzati cooperanti (TCA) (8)
Un run R è una sequenza di configurazioni globali C0 , C1, …, Ci ,
…
tale che C0 è iniziale e Cj C Cj+1 per j  0. Se Inf(R) è l’insieme di
stati attraversati infinite volte il run ha successo se Inf(R)  F  .
Un ambiente è accettato da un TCA se esiste un run di successo a
a partire dalla configurazione iniziale con ambiente a.
Il linguaggio accettato dal TCA è l’insieme dei run di successo.
Automi temporizzati cooperanti (TCA) (9)
q1
a,True
q2
True, q2[m]
q3
a,q3=0
q4
a,True
a,True
F = {q4}
True, q2[m]
Automi temporizzati cooperanti (TCA) (10)
M1
St1
q1
Start
Not good
and trash
Q2[3]and
St2[3]
M2
(w1 or w2)
and in q1[5]
Tr1[0]
good
Q2[1]and
St2[1]
St2
Tr1
q3[1]
q3
St2[0]
St1[0]
q2
cool
Tr2
La macchina M1 riceve materiale rozzo e produce un
prodotto finale, la macchina M2 fornisce a M1 il
materiale e poi raccoglie il prodotto finale.
Automi temporizzati cooperanti (TCA) (11)
La macchina M1 finchè M2 è in grado di fornire il materiale
(stato Tr1 abilitato) e l’ambiente dà il segnale start. Allora M1 fa
la lavorazione se il materiale è presente (segnale in) e c’è una
richiesta di produrre il prodotto finale p1 (segnale w1) oppure il
prodotto finale p2 (segnale w2). Dopo almeno 5 unità di tempo il
prodotto è completo (stato St2 abilitato) e la macchina M2
raggiunge uno stato in cui può raccoglierlo. Dopo una fase di
raffreddamento M1 verifica la qualità del prodotto e raggiunge lo
stato St1 in una unità di tempo se il prodotto è buono, in tre unità
di tempo altrimenti. Dopo questa transizione di M1, M2 raccoglie
il prodotto e dopo almeno una unità di tempo fornisce a M1
nuovo materiale.
Proprietà di chiusura
Siano M, M’ TCA. Allora
L(M)  L(M’) = L(M  M’)
L(M)  L(M’) = L(M  M’)
Si ha chiusura per complementazione?
Risultati di espressività (1)
Gli automi con vincoli di orologio periodici TAP hanno vincoli
ottenuti applicando liberamente connettivi booleani a
proposizioni atomiche x  Ts[t1, t2] dove x è un orologio e
Ts[t1, t2] = { ks + t; k  N, t1 ≤ t ≤ t2 } per s, t1, t2  Time.
a, x T2[0,0], x:=0
a, true, x:=0
Risultati di espressività (2)
Gli automi con transizioni silenti TAe hanno transizioni in
E  SSS{e}2Cf(C).
e, t1≤x≤t2, x:=0
a, true, x:=0
a, x= 0
Vale
L(TA)  L(TAp)  L(TAe)
Risultati di espressività (3)
Sia TCAI un TCA con soli stati di input. Sia STCA un TCA
consistente di un solo automa sequenziale. Vale
L(STCAIRU)

|
L(TA)
|

|
L(TCAIRU)
L(TCARU)
L(TAP)
|

 L(TAe)
|
L(TCAU)
L(TCAR)
|
|
L(STCAU)  L(STCARU)  L(STCAR)
|
L(STCA)
Risultati di decisione
La vuotezza è decidibile per L(STCAIRU).
Prova. Dalla contenutezza di L(STCAIRU) in L(TA).