Ajastatud automaadid

Sissejuhatus

Ajastatud automaadid ehk ajastatud olekumasinad (timed automata) täiendavad lõplike automaatide ehk lõplike olekumasinate (finite automata ehk state machine) konseptsiooni kellaga (clock). Kellad jooksevad jätkuvalt (continuously) ning sama kiirusega (synchronous, uniform). Kellasi võib lähtestada (reset to zero) ülemineku korral. Kell mõjutab missugused üleminekud (transitions) toimuda võivad (clock conditions). Kell kuulub positiivsete reaalarvude ning 0 hulka.

Üleminekutel on valvur (guard) mis võimaldab edusammude tegemist. Ülemineku toimumiseks peab kell rahuldama valvuri tingimusi. Olekutel (states) on invariandid mis tagavad edusammud (ensure progress). Invariandi rikkumist saab vältida üleminekuga järgmisse olekusse.

Kellad x, y, z, ... kuuluvad kellade hulka C. Kella väärtustamine v(x) omistab mitte-negatiivse reaalarvulise väärtuse kellale x. Φ(C) tähistab kellade kitsendusi üle hulga C. Kellade kitsendused on kujul x ≃ d või x – y ≃ d kus d on naturaalarv.

Formaalne notatsioon

Ajastatud automaadi võib kirja panna ka kui korteeži (tuple):

\begin{equation*} TA = (L, Lₒ, E, C, Inv, T) \end{equation*}

Kus L on lõplik olekute (location) hulk. Ajastatud automaadis eristatakse kahte olekut (state vs location) kuna aeg mängib rolli:

\begin{equation*} L = \{L_1, L_2, L_3, ..., L_n\} \end{equation*}

Ning Lₒ on esialgsete asukohtade hulk:

\begin{equation*} L_0 \subseteq L \end{equation*}

E on lõplik sündmuste hulk:

\begin{equation*} E \equiv sündmused \end{equation*}

C on ajastatud automaadi TA lõplik kellade hulk:

\begin{equation*} C = \{ C_1, C_2, C_3, ..., C_n \} \end{equation*}

Inv on funktsioon mis omistab igale asukohale invariandi. Invariant on hulk väiteid mis peavad kehtima selles olekus (?):

\begin{equation*} Inv: L \rightarrow \Phi (C) \end{equation*}

T on ülemineku seos:

\begin{equation*} T \subseteq L \times E \times \Phi(C) \times \Gamma(C) \times L \end{equation*}

Täpsustuseks üleminek t tähistab serve olekust l₁ olekusse l₂ sildiga e, valvurite (guard) φ(C) ning kellade lähtestamistega γ(C):

\begin{equation*} t = (l_1, e, \varphi(C), \gamma(C), l_2) \end{equation*}

Φ(C) tähistab kellade tinigmusi (clock conditions) üle kellade hulga (clock set).

Semantika

Ajastatud automaadis semantiline olek (semantic state) sõltub olekust (location) ning kellade vektorist (vector of clock values). Semantilisi üleminekuid on kahesuguseid.

Esiteks ajasammu (time step) puhul automaat jääb samasse olekusse (location) ning kellade väärtusi suurendatakse δ võrra. Seda võib ka interpreteerida kui viivitust (delay):

\begin{equation*} (l, v) \xrightarrow{\delta} (l, v + \delta) \end{equation*}

Teist tüüpi semantiline üleminek on diskreetne üleminek (discrete transition):

\begin{equation*} (l, v) \xrightarrow{e} (l^\prime, v^\prime) \end{equation*}

Tee (path) on lõplik või lõpmatu diskreetsete üleminekute ja ajasammude järjestus:

\begin{equation*} (l_0, v_0) \xrightarrow{e_0} (l_1, v_1) \xrightarrow{e_1} (l_2, v_2) \xrightarrow{e_2} (l_3, v_3) \xrightarrow{e_3} ... \end{equation*}

Ajastatud automaat Kripke struktuurina

Semantilised olekuid (ajasammud ning diskreetseid üleminekuid) võib üles märkida Kripke struktuurina:

\begin{equation*} (Q, \rightarrow, S) \end{equation*}

Kus Q on semantiline olek mis rahuldab oleku invariandi tingimusi:

\begin{equation*} Q := \{ (l,v) \in L \times V_C | v \models Inv(l) \} \end{equation*}

Üleminekusuhe on defineeritud kui üleminek ühest semantilisest olekust teise, kas sündmuse E või aja kulgemise tõttu (?).

\begin{equation*} \rightarrow \subseteq Q \times (E \cup \mathbb{R}^{+}) \times Q \end{equation*}

Ning S on esialgsete semantiliste olekute hulk:

\begin{equation*} S := \{ (l_0, v_0 ) \in L \times V_C | v_0 \models Inv(l_0) \} \end{equation*}

Samaaegsed ajastatud masinad

Kaks ajastatud masinat saab sündmustega siduda. Sündmuse saatja c! ning sündmuse vastuvõtja c?. Sündmuste saatmine on realiseeritud valvurite (guard) näol.

Kaks automaati saab formaalselt kirja panna kui:

\begin{equation*} TA_1 || TA_2 := (L_1 \times L_2, L_{0,1} \times L_{0,2}, E_1 \cup E_2, C_1 \cup C_2, Inv, T) \end{equation*}

Kus mõlema automaadi invariandid peavad olema rahuldatud:

\begin{equation*} Inv(s_1, s_2) = Inv(s_1) \land Inv(s_2) \end{equation*}

Komposiitüleminekud sünkroniseerimiseks:

\begin{equation*} t := ((l_1, l_2), e_1, \phi_1(C) \land \phi_2(C), \gamma_1(C) \land \gamma_2(C), (l_1^\prime, l_2^\prime)),\ kui\ e_1 = e_2 \in E_1 \cap E_2 \end{equation*}

Esimesest automaadist sõltumatud üleminekud:

\begin{equation*} t := ((l_1, l_2), e_1, \phi_1(C), \gamma_1(C), (l_1^\prime, l_2)),\ kui\ e_1 \notin \in E_1 \cap E_2 \end{equation*}

Teisest automaadist sõltumatud üleminekud:

\begin{equation*} t := ((l_1, l_2), e_2, \phi_2(C), \gamma_2(C), (l_1, l_2^\prime)),\ kui\ e_2 \notin \in E_1 \cap E_2 \end{equation*}

Kaksiksünkroniseerimine (binary synchronization) on blokeeriv (blocking communication): Kui üks kommunikatsiooni paarilistest pole valmis siis teine peab ootama. Lähtuvalt sellest c! ning c? vallanduvad (event fired) ühes sammus.

Üldlevisünkroniseerimine (broadcast synchronization) on asünkroonne (non-blocking communication). Kes iganes on valmis vastu võtma reageerib sündmuse peale, ülejäänud magavad maha.

QAoES TU Berlin