Omega automat

Un automat ω sau automat pe cuvinte infinite este, în informatică teoretică și mai ales în teoria automatelor , este un automat cu stare finită care acceptă cuvinte de lungime infinită.

Automatele pe cuvinte infinite sunt utilizate pentru a modela calcule care nu se finalizează, cum ar fi comportamentul unui sistem de operare sau a unui sistem de control. Pentru astfel de sisteme, este posibil să se specifice proprietăți precum „fiecare cerere va fi urmată de un răspuns” sau respingerea acesteia „există o cerere care nu este urmată de un răspuns” în contextul verificării modelului . Astfel de proprietăți pot fi formulate pentru cuvinte infinite și pot fi verificate de automatele finite.

Au fost introduse mai multe clase de automate pe cuvinte de lungime infinită: automate Büchi , automate Rabin, automate Streett , automate egale , automate Muller și, pentru fiecare clasă, versiuni deterministe sau nedeterministe. Aceste clase diferă numai în condițiile de acceptare. Toate aceste clase, cu excepția notabilă a automatelor Büchi deterministe, recunosc aceeași familie de seturi de cuvinte infinite, numite seturi regulate de cuvinte infinite sau limbaje ω-regulate . Aceste automate, chiar dacă acceptă aceleași limbi, pot varia ca dimensiune într-o anumită limbă.

Definiție

În ceea ce privește automatele finite , un automat pe cuvinte infinite ${\mathcal {A}}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ mathcal {A}}$ pe un alfabet $\Sigma$ ${\ displaystyle \ Sigma}$ $\ Sigma$ este dat de ${\mathcal {A}}=(Q,{\mathcal {F}},I,T)$ ${\ displaystyle {\ mathcal {A}} = (Q, {\ mathcal {F}}, I, T)}$ ${\ displaystyle {\ mathcal {A}} = (Q, {\ mathcal {F}}, I, T)}$ astfel încât

$Î$ ${\ displaystyle Q}$ $Î$ este un set finit de stări,
${\mathcal {F}}\subseteq Q\times A\times Q$ ${\ displaystyle {\ mathcal {F}} \ subseteq Q \ times A \ times Q}$ ${\ displaystyle {\ mathcal {F}} \ subseteq Q \ times A \ times Q}$ este setul de tranziții,
$I\subseteq Q$ ${\ displaystyle I \ subseteq Q}$ ${\ displaystyle I \ subseteq Q}$ este setul de stări inițiale,
$T\subseteq Q$ ${\ displaystyle T \ subseteq Q}$ ${\ displaystyle T \ subseteq Q}$ este un set de stări finale sau terminale.

Se presupune adesea că setul de stări inițiale este compus dintr-un singur element. O tranziție $f=(p,a,q)\in {\mathcal {F}}$ ${\ displaystyle f = (p, a, q) \ în {\ mathcal {F}}}$ ${\ displaystyle f = (p, a, q) \ în {\ mathcal {F}}}$ este alcătuit dintr-o stare de plecare $p$ ${\ displaystyle p}$ $p$ , o eticheta $la$ ${\ displaystyle a}$ $la$ și o stare de sosire $q$ ${\ displaystyle q}$ $q$ . Un calcul $c$ ${\ displaystyle c}$ $c$ (numită și cale sau pistă ) este o serie infinită de tranziții consecutive:

c=(p_{0},a_{1},p_{1})(p_{1},a_{2},p_{2})\cdots

{\ displaystyle c = (p_ {0}, a_ {1}, p_ {1}) (p_ {1}, a_ {2}, p_ {2}) \ cdots}

{\ displaystyle c = (p_ {0}, a_ {1}, p_ {1}) (p_ {1}, a_ {2}, p_ {2}) \ cdots}

Pentru $c$ ${\ displaystyle c}$ $c$ , starea inițială este $p_{0}$ ${\ displaystyle p_ {0}}$ $p_ {0}$ , eticheta sa este cuvântul infinit $a_{1}a_{2}\cdots a_{n}\cdots$ ${\ displaystyle a_ {1} a_ {2} \ cdots a_ {n} \ cdots}$ ${\ displaystyle a_ {1} a_ {2} \ cdots a_ {n} \ cdots}$ . Calculul are succes și cuvântul este acceptat (sau recunoscut de automat) dacă trece infinit de des printr-o stare terminală.

Se spune că un automat este determinist dacă îndeplinește următoarele două condiții:

are o singură stare inițială;
pentru fiecare stat $q$ ${\ displaystyle q}$ $q$ și pentru fiecare literă $la$ ${\ displaystyle a}$ $la$ , există cel mult o tranziție care începe de la $q$ ${\ displaystyle q}$ $q$ și purtând eticheta $la$ ${\ displaystyle a}$ $la$ .

Condiția de acceptare

Pentru un calcul $c$ ${\ displaystyle c}$ $c$ , ${\rm {Inf}}(c)$ ${\ displaystyle {\ rm {Inf}} (c)}$ ${\ displaystyle {\ rm {Inf}} (c)}$ este ansamblul stărilor care apar de un număr infinit de ori în $c$ ${\ displaystyle c}$ $c$ . Acest concept face posibilă formularea condițiilor de acceptare.

Automate Büchi

Același subiect în detaliu: automatul lui Büchi .

Condiția de acceptare este: ${\mathcal {A}}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ mathcal {A}}$ acceptă un cuvânt infinit dacă și numai dacă este eticheta unui calcul $c$ ${\ displaystyle c}$ $c$ pentru care ${\rm {Inf}}(c)$ ${\ displaystyle {\ rm {Inf}} (c)}$ ${\ displaystyle {\ rm {Inf}} (c)}$ conține cel puțin o stare finală, deci astfel încât ${\rm {Inf}}(c)\cap T\neq \emptyset$ ${\ displaystyle {\ rm {Inf}} (c) \ cap T \ neq \ emptyset}$ ${\ displaystyle {\ rm {Inf}} (c) \ cap T \ neq \ emptyset}$ .

Automatul lui Rabin

Un automat Rabin este definit cu un set $\Omega$ ${\ displaystyle \ Omega}$ $\Omega$ de perechi de seturi de stări $(E,F)$ ${\ displaystyle (E, F)}$ ${\ displaystyle (E, F)}$ . Condiția de acceptare este: ${\mathcal {A}}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ mathcal {A}}$ acceptă un cuvânt infinit w dacă și numai dacă w este eticheta unui calcul pentru care există o pereche $(E,F)$ ${\ displaystyle (E, F)}$ ${\ displaystyle (E, F)}$ din $\Omega$ ${\ displaystyle \ Omega}$ $\Omega$ pentru care ${\rm {Inf}}(c)\cap E=\emptyset$ ${\ displaystyle {\ rm {Inf}} (c) \ cap E = \ emptyset}$ ${\ displaystyle {\ rm {Inf}} (c) \ cap E = \ emptyset}$ Și ${\rm {Inf}}(c)\cap F\neq \emptyset$ ${\ displaystyle {\ rm {Inf}} (c) \ cap F \ neq \ emptyset}$ ${\ displaystyle {\ rm {Inf}} (c) \ cap F \ neq \ emptyset}$ .

Automatul lui Streett

Un automat Streett este definit cu un set $\Omega$ ${\ displaystyle \ Omega}$ $\Omega$ de perechi de seturi de stări $(E,F)$ ${\ displaystyle (E, F)}$ ${\ displaystyle (E, F)}$ . Condiția de acceptare este: ${\mathcal {A}}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ mathcal {A}}$ acceptă un cuvânt infinit w dacă și numai dacă w este eticheta unui calcul pentru care, pentru orice pereche $(E,F)$ ${\ displaystyle (E, F)}$ ${\ displaystyle (E, F)}$ din $\Omega$ ${\ displaystyle \ Omega}$ $\Omega$ , da ${\rm {Inf}}(c)\cap E\neq \emptyset$ ${\ displaystyle {\ rm {Inf}} (c) \ cap E \ neq \ emptyset}$ ${\ displaystyle {\ rm {Inf}} (c) \ cap E \ neq \ emptyset}$ Și ${\rm {Inf}}(c)\cap F=\emptyset$ ${\ displaystyle {\ rm {Inf}} (c) \ cap F = \ emptyset}$ ${\ displaystyle {\ rm {Inf}} (c) \ cap F = \ emptyset}$ ^[1] .

Starea lui Streett este negarea stării lui Rabin. Prin urmare, un automat Streett determinist acceptă exact complementul setului acceptat de automatul Rabin determinist pe același set $\Omega$ ${\ displaystyle \ Omega}$ $\Omega$ .

Automatul egalității

Un automat de paritate este un automat ale cărui stări sunt numerotate. Condiția de acceptare este: ${\mathcal {A}}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ mathcal {A}}$ acceptă un cuvânt infinit w dacă și numai dacă w este eticheta unui calcul în care cel mai mic dintre numerele întregi din ${\rm {Inf}}(c)$ ${\ displaystyle {\ rm {Inf}} (c)}$ ${\ displaystyle {\ rm {Inf}} (c)}$ este uniform .

Automatul lui Muller

Un automat Muller este definit cu o familie ${\mathcal {M}}$ ${\ displaystyle {\ mathcal {M}}}$ $\ mathcal {M}$ a seturilor de stări. Condiția de acceptare este: ${\mathcal {A}}$ ${\ displaystyle {\ mathcal {A}}}$ ${\ mathcal {A}}$ acceptă un cuvânt infinit dacă și numai dacă este eticheta unui calcul astfel încât ${\rm {Inf}}(c)\subseteq {\mathcal {M}}$ ${\ displaystyle {\ rm {Inf}} (c) \ subseteq {\ mathcal {M}}}$ ${\ displaystyle {\ rm {Inf}} (c) \ subseteq {\ mathcal {M}}}$ .

Orice automat Büchi poate fi văzut ca un automat Muller: pur și simplu luați-l ca ${\mathcal {M}}$ ${\ displaystyle {\ mathcal {M}}}$ $\ mathcal {M}$ toate subseturile de $Î$ ${\ displaystyle Q}$ $Î$ care conține cel puțin o stare terminală. Dimpotrivă, pentru fiecare automat Muller a $n$ ${\ displaystyle n}$ $n$ stări și $m$ ${\ displaystyle m}$ $m$ seturi de acceptare, există cel mult un automat Büchi echivalent cu cel mult $n+mn2^{n}$ ${\ displaystyle n + mn2 ^ {n}}$ ${\ displaystyle n + mn2 ^ {n}}$ State. În mod similar, automatele Rabin, Streett și parity pot fi privite ca automate Muller.

Puterea expresivă

Un limbaj infinit de cuvinte sau limbajul is este un set de cuvinte de lungime infinită pe un alfabet dat. Puterea expresivă a unui automat is este măsurată de clasa tuturor limbajelor ω care pot fi recunoscute de automat. Automatele Büchi nedeterministe, paritatea, Rabin, Streett și Muller recunosc toate aceleași limbi, care sunt limbi regular-regulate . Se poate demonstra că automatele de paritate deterministe ale lui Rabin, Streett și Muller recunosc aceleași limbaje, spre deosebire de automatismele Büchi deterministe. Rezultă în special că clasa limbajelor ω este închisă prin complementare.

Exemplu

Automat Büchi nedeterministic care recunoaște cuvinte infinite cu un număr finit de

la

{\ displaystyle a}

la

.

Automatul din figură recunoaște setul de cuvinte de lungime infinită de pe alfabet format din două litere $la$ ${\ displaystyle a}$ $la$ Și $b$ ${\ displaystyle b}$ $b$ care conțin un număr finit de litere $la$ ${\ displaystyle a}$ $la$ , adică întregul $\{a,b\}^{*}b^{\omega }$ ${\ displaystyle \ {a, b \} ^ {*} b ^ {\ omega}}$ ${\ displaystyle \ {a, b \} ^ {*} b ^ {\ omega}}$ . De fapt, pentru fiecare cuvânt de acest tip $\{a,b\}^{*}b^{\omega }$ ${\ displaystyle \ {a, b \} ^ {*} b ^ {\ omega}}$ ${\ displaystyle \ {a, b \} ^ {*} b ^ {\ omega}}$ , există o execuție a automatului care se repetă în starea q, care este terminală.

Se arată că nu există un automat Büchi determinist care să accepte limbajul $\{a,b\}^{*}b^{\omega }$ ${\ displaystyle \ {a, b \} ^ {*} b ^ {\ omega}}$ ${\ displaystyle \ {a, b \} ^ {*} b ^ {\ omega}}$ . Automatele Büchi deterministe sunt strict mai puțin expresive decât automatele Büchi nedeterministe ^[2] .

Notă

^ Farwer , p. 7 .
^ Christel Baier și Joost-Pieter Katoen, Principiile verificării modelelor (seria de reprezentare și minte) , The MIT Press, 31 mai 2008, pp. 191, 975, ISBN 978-0-262-02649-9 .

Bibliografie

( EN ) Berndt Farwer, ω-Automata , în Erich Grädel, Wolfgang Thomas și Thomas Wilke (ed.), Logici automat și jocuri infinite: Un ghid pentru cercetările actuale ,, Lecture Notes in Computer Science , n. 2500, Springer-Verlag New York, Inc., 1 ianuarie 2002, pp. 3-22, ISBN 978-3-540-00388-5 .
( EN ) Wolfgang Thomas, Automate on infinite objects , în Jan Van Leeuwen (ed.), Handbook of Theoretical Computer Science: Formal Models and Semantics , t. B, MIT Press, 1990, pp. 133-192, ISBN 0-262-72015-9 .
( EN ) Dominique Perrin și Jean-Éric Pin, Infinite Words , Elsevier, 2004, p. 538, ISBN 978-0-12-532111-2 .

Elemente conexe

linkuri externe

Paritosh K. Pandya, Automate on Infinite Words ( PDF ), pe tcs.tifr.res.in.
Yann Pequignot, Automate, Limbi și logică ( PDF ), pe hec.unil.ch , Școala Politehnică Federală din Lausanne, 2009.

Portal IT : accesați intrările Wikipedia care se ocupă cu IT

[1] Farwer , p. 7 .

[2] Christel Baier și Joost-Pieter Katoen, Principiile verificării modelelor (seria de reprezentare și minte) , The MIT Press, 31 mai 2008, pp. 191, 975, ISBN 978-0-262-02649-9 .

[1]

[2]