Uogólniony automat Büchiego

W teorii automatów uogólniony automat Büchiego jest wariantem automatu Büchiego . Różnica w stosunku do automatu Büchiego polega na warunku akceptacji, który jest określony przez zbiór zbiorów stanów. Przebieg jest akceptowany przez automat, jeśli nieskończenie często odwiedza co najmniej jeden stan każdego zestawu warunku akceptującego. Uogólnione automaty Büchiego są równoważne pod względem mocy ekspresyjnej automatom Büchiego; tu transformacja .

W weryfikacji formalnej metoda sprawdzania modelu wymaga uzyskania automatu z formuły LTL , który określa pożądaną właściwość programu. Istnieją algorytmy , które tłumaczą formułę LTL na uogólniony automat Büchi. w tym celu. Pojęcie uogólnionego automatu Büchiego zostało wprowadzone specjalnie na potrzeby tego tłumaczenia.

Definicja formalna

₀ Formalnie uogólniony automat Büchi to krotka , która składa się z następujących elementów: ZA = ( Q , Σ, Δ, Q , ${\ displaystyle {\ cal {F}}}}$

• Q jest skończonym zbiorem . Elementy Q nazywane są stanami A .
• Σ jest skończonym zbiorem zwanym alfabetem A .
• Δ: Q × Σ → 2 Q ^jest funkcją, zwaną relacją przejścia A .
• ₀ Q jest podzbiorem Q , zwanym stanami początkowymi.
• $jest$ warunkiem akceptacji , który składa się z zera lub więcej zestawów akceptujących $_$ zestaw podzbiorem . _

A akceptuje dokładnie te przebiegi, w których zbiór nieskończenie często występujących stanów zawiera co najmniej jeden stan z każdego zbioru akceptującego ${\ Displaystyle F_ {i} \ in {\ cal {F}}}$ . Zauważ, że może nie być zestawów akceptujących, w którym to przypadku każdy nieskończony przebieg trywialnie spełnia tę właściwość.

Aby zapoznać się z bardziej wszechstronnym formalizmem, zobacz także ω-automat .

Oznaczony uogólniony automat Büchi

Oznaczony uogólniony automat Büchiego to kolejna odmiana, w której dane wejściowe są dopasowywane do etykiet na stanach , a nie na przejściach. Został wprowadzony przez Gertha i in.

₀ Formalnie oznaczony uogólniony automat Büchi to krotka ), która składa się z następujących elementów: ZA = ( Q , Σ, L , Δ, Q , ${\ displaystyle {\ cal {F}}}}$

• Q jest skończonym zbiorem . Elementy Q nazywane są stanami A .
• Σ jest skończonym zbiorem zwanym alfabetem A .
• L : Q → 2 Σ ^jest funkcją, zwaną funkcją etykietowania A .
• Δ: Q → 2 ^Q jest funkcją, zwaną relacją przejścia A .
• ₀ Q jest podzbiorem Q , zwanym stanem początkowym.
• $jest$ warunkiem akceptacji , który składa się z zera lub więcej zestawów akceptujących Każdy zestaw akceptujący jest podzbiorem Q . ${\ displaystyle F_ {i} \ in {\ cal {F}}}$

₀ Niech w = a ₁ a ₂ ... będzie słowem ω nad alfabetem Σ. Sekwencja r ₁ , r ₂ , ... jest ciągiem A na słowie w , jeśli r ₁ ∈ Q i dla każdego i ≥ 0, r _{i +1} ∈ Δ( r _i ) oraz a _i ∈ L ( r _i ). A akceptuje dokładnie te przebiegi, w których zbiór nieskończenie często występujących stanów zawiera co najmniej jeden stan z każdego zbioru akceptującego ${\ Displaystyle F_ {i} \ in {\ cal {F}}}$ . Zauważ, że może nie być zestawów akceptujących, w którym to przypadku każdy nieskończony przebieg trywialnie spełnia tę właściwość.

Aby uzyskać wersję bez etykiet, etykiety są przenoszone z węzłów do przejść przychodzących.