timed automaton

Angol

Főnév

timed automaton (tsz. timed automatons)

(informatika) A timed automaton (időzített automata) a formális módszerek és valós idejű rendszerek modellezésének egyik központi eszköze. Ez a modell az egyszerű végállapot-automaták kibővítése, ahol a viselkedés már nemcsak az események sorrendjétől, hanem azok időzítésétől is függ. A timed automaton segítségével pontosan modellezhetők olyan rendszerek, ahol a helyes működés időkorlátokhoz kötött — például protokollok, vezérlőrendszerek, embedded rendszerek, közlekedési szimulációk.

1. Bevezetés: Mi az a timed automaton?

Egy timed automaton egy állapotgép, amely:

rendelkezik órákkal (clocks),
az átmenetekhez és állapotokhoz időzítési feltételeket rendel (pl. „csak akkor lépj tovább, ha 5 másodperc eltelt”),
és az órák értékét újraindíthatja (reset) bizonyos átmenetek során.

Ezáltal kvantitatív időfüggő viselkedést lehet formálisan leírni és elemezni.

2. Formális definíció

Egy timed automaton egy ötös:

$A=(L,l_{0},C,\Sigma ,E)$

ahol:

${\textstyle L}$ : véges halmaz az állapotokkal (location)
${\textstyle l_{0}\in L}$ : kezdeti állapot
${\textstyle C}$ : véges halmaz az órákkal (pl. ${\textstyle x,y,z}$ )
${\textstyle \Sigma }$ : bemeneti ábécé (események)
${\textstyle E\subseteq L\times \Sigma \times G(C)\times 2^{C}\times L}$ ${\textstyle E\subseteq L\times \Sigma \times G(C)\times 2^{C}\times L}$ : átmenetek halmaza Minden átmenet:
- egy forrásállapotból indul,
- egy eseményhez kapcsolódik,
- van egy őr (guard), amely az órákra vonatkozó feltétel,
- nullázhat bizonyos órákat (reset),
- célállapotba visz.

Példa egy őrre (guard):

$x\leq 5$

→ Az átmenet csak akkor hajtható végre, ha az „x” óra értéke legfeljebb 5.

3. Órák és idő múlása

Az órák folyamatosan növekednek, amíg az automaton egy adott állapotban „várakozik”. Amikor egy átmenet végrehajtódik:

az idő nem halad, az átmenet pillanatnyi,
bizonyos órák értékét lenullázhatjuk.

Az idő „óraérték-konfigurációként” jelenik meg: minden óra egy nemnegatív valós szám értéket hordoz.

4. Timed automaton működése

A rendszer működése kétféleképpen haladhat:

Idő múlása: a rendszer az aktuális állapotban marad, minden óra nő azonos mértékben.
Diszkrét átmenet: ha teljesül az átmenethez tartozó feltétel (guard), akkor lépés történik, és az adott órák újraindulhatnak.

5. Állapottér: végtelen, de kezelhető

Mivel az órák valós számértéket vehetnek fel, a timed automaton állapotertere elvileg végtelen. Azonban zónákra (absztrakt időtartományokra) osztva végeselemű állapottér-analízis is lehetséges (pl. region graph, zone graph).

6. Felhasználási területek

Valós idejű protokollok: például Token Ring, CSMA/CD.
Embedded rendszerek: érzékelőkkel, határidőkkel, reakcióidőkkel.
Automatikus vezérlők: például liftek, robotkarok, gyártósorok.
Közlekedésirányítás: jelzőlámpák, vonatirányítás.
Szoftver modellellenőrzés (model checking): a szoftver „időben” helyesen működik-e?

7. Eszközök és implementáció

UPPAAL

A legismertebb eszköz timed automaton modellezésére és verifikációjára:

Grafikus interfész
Formális tulajdonságok vizsgálata: „az esemény legfeljebb 5 másodpercen belül megtörténik-e?”
Tulajdonságok kifejezése TCTL nyelven (timed computation tree logic)

8. Példa: Riasztóóra modell

Állapotok:

Idle – nyugalmi állapot
Waiting – időzítés alatt
Beep – megszólal a riasztó

Óra: x

Átmenetek:

Idle → Waiting [gombnyomás / reset x]
Waiting → Beep [x ≥ 10]
Beep → Idle [befejezés / reset x]

Ez egy egyszerű reaktív időzítő, amely 10 másodpercen belül reagál a bemenetre.

9. Előnyök

Formális biztonság: precíz, matematikailag igazolható modellek.
Model checking támogatása: automatikus hibadetektálás.
Időkritikus rendszerek verifikációja lehetséges (pl. “határidőre elvégzett feladatok”).
Egyszerű vizuális ábrázolhatóság, intuitív értelmezés.

10. Korlátok és kihívások

Állapottér-robbanás: időtartományokkal az elemzés költséges lehet.
Real-time absztrakciók néha túlzottan leegyszerűsítettek.
Nem determinisztikus viselkedés kezelése nehéz lehet.

Összefoglalás

A timed automaton egy elegáns és erőteljes eszköz valós idejű rendszerek modellezésére. Az automatákban használt órák és időzítési feltételek segítségével pontosan reprezentálhatjuk a fizikai világ időbeli korlátait és követelményeit. Legyen szó beágyazott szoftverről, kommunikációs protokollról vagy vezérlőrendszerről, a timed automaton egy bizonyíthatóan helyes működésre alkalmas eszköz, amely a formális verifikáció és a megbízható szoftverfejlesztés egyik pillére.

További információk

timed automaton - Szótár.net (en-hu)
timed automaton - Sztaki (en-hu)
timed automaton - Merriam–Webster
timed automaton - Cambridge
timed automaton - WordNet
timed automaton - Яндекс (en-ru)
timed automaton - Google (en-hu)
timed automaton - Wikidata
timed automaton - Wikipédia (angol)