Büchiho automat

Technology

12 hours ago

Author

Büchiho automat je typem nedeterministického Buchiho automatu používaného v teorii formálních jazyků. Byl pojmenován po svém tvůrci, Jiřím Büchim, který jej popsal v roce 1960. Tento automat slouží k rozpoznávání jazyků nad nekonečnými slovy. Büchiho automat má obecně pouze nekonečně mnoho koncových stavů a na vstupní pásce přijímá nekonečné řetězce symbolů. Jazyk přijímaný Büchiho automatem je definován jako množina všech nekonečných řetězců, které přijme automat. Büchiho automaty jsou velmi důležité ve formálních metodách a automatonické logice a mají široké uplatnění v oblastech jako verifikace software, syntaktická analýza programů a model checking.

Büchiho automat je v teorii automatů ω-automat, který rozšiřuje koncept konečného automatu pro nekonečné vstupy (slova nekonečné délky). Büchiho automat akceptuje slovo, pokud existuje běh automatu, který navštíví alespoň jeden koncový stav nekonečněkrát. Automat je pojmenován po švýcarském matematikovi Juliovi Richardu Büchim, který ho vynalezl v roce 1962.

Formální definice

Deterministický Büchiho automat je pětice A = (Q,Σ,δ,q0,F) skládající se z těchto komponent: * Q je konečná množina stavů * Σ je konečná množina znaků - abeceda automatu A * δ: Q × Σ → Q je přechodová funkce * q0 je prvek množiny Q - začáteční stav automatu A * F ⊆ Q je množina koncových stavů; automat akceptuje slovo, pokud je alespoň jeden z koncových stavů navštíven nekonečněkrát

Nedeterministický Büchiho automat je podobný deterministickému, ale přechodová funkce Δ odkazuje na množinu stavů (místo jednoho konkrétního stavu) a začáteční stav q0 je nahrazen množinou začátečních stavů I. Obecně pojem Büchiho automat bez přívlastku označuje právě nedeterministický Büchiho automat.