En la teoría de autómatas , un autómata Büchi semideterminista (también conocido como autómata Büchi determinista en el límite [ 1] o autómata Büchi determinista en el límite [2] ) es un tipo especial de autómata Büchi . En un autómata de este tipo, el conjunto de estados se puede dividir en dos subconjuntos: un subconjunto forma un autómata determinista y también contiene todos los estados aceptantes.
Para cada autómata Büchi, se puede construir un autómata Büchi semideterminista de modo que ambos reconozcan el mismo ω-lenguaje . Sin embargo, puede que no exista un autómata Büchi determinista para el mismo ω-lenguaje.
En la comprobación de modelos estándar frente a las propiedades de la lógica temporal lineal (LTL), es suficiente traducir una fórmula LTL a un autómata Büchi no determinista. Sin embargo, en la comprobación de modelos probabilísticos, las fórmulas LTL se traducen normalmente a autómatas Rabin deterministas (DRA), como por ejemplo en la herramienta PRISM . Sin embargo, no se necesita un autómata completamente determinista. De hecho, los autómatas Büchi semideterministas son suficientes en la comprobación de modelos probabilísticos.
Un autómata Büchi (Q,Σ,∆,Q 0 ,F) se llama semideterminista si Q es la unión de dos subconjuntos disjuntos N y D tales que F ⊆ D y, para cada d ∈ D, el autómata (D,Σ,∆,{d},F) es determinista.
Cualquier autómata Büchi dado puede transformarse en un autómata Büchi semideterminista que reconoce el mismo lenguaje, utilizando la siguiente construcción.
Supóngase que A = (Q, Σ, ∆, Q 0 , F) es un autómata de Büchi. Sea Pr una función de proyección que toma un conjunto de estados S y un símbolo a ∈ Σ y devuelve un conjunto de estados {q' | ∃q ∈ S y (q, a, q') ∈ ∆ }. El autómata de Büchi semideterminista equivalente es A' = (N ∪ D, Σ, ∆', Q' 0 , F'), donde
Nótese la estructura de estados y transiciones de A′ . Los estados de A′ se dividen en N y D. Un estado N se define como un elemento del conjunto potencia de estados de A . Un estado D se define como un par de elementos del conjunto potencia de estados de A . La relación de transición de A' es la unión de cuatro partes: ∆ 1 , ∆ 2 , ∆ 3 y ∆ 4 . Las transiciones ∆ 1 solo llevan a A' de un estado N a un estado N. Solo las transiciones ∆ 2 pueden llevar a A' de un estado N a un estado D. Nótese que solo las transiciones ∆ 2 pueden causar no determinismo en A' . Las transiciones ∆ 3 y ∆ 4 llevan a A' de un estado D a un estado D. Por construcción, A' es un autómata Büchi semideterminista. La prueba de L(A')=L(A) se deduce de lo anterior.
Para una ω-palabra w =a 1 ,a 2 ,... , sea w (i,j) el segmento finito a i+1 ,...,a j-1 ,a j de w .
Demostración: Sea w ∈ L(A'). El estado inicial de A' es un estado N y todos los estados aceptantes en F' son estados D. Por lo tanto, cualquier serie aceptante de A' debe seguir ∆ 1 durante un número finito de transiciones al inicio, luego tomar una transición en ∆ 2 para pasar a estados D, y luego tomar ∆ 3 y ∆ 4 transiciones para siempre. Sea ρ' = S 0 ,...,S n-1 ,(L 0 ,R 0 ),(L 1 ,R 1 ),... dicha serie aceptante de A' en w .
Por definición de ∆ 2 , L 0 debe ser un conjunto singleton. Sea L 0 = {s}. Debido a las definiciones de ∆ 1 y ∆ 2 , existe un prefijo de serie s 0 ,...,s n-1 ,s de A en la palabra w(0,n) tal que s j ∈ S j . Como ρ' es una serie de aceptación de A' , algunos estados en F' se visitan infinitamente a menudo. Por lo tanto, existe una secuencia estrictamente creciente e infinita de índices i 0 ,i 1 ,... tales que i 0 =0 y, para cada j > 0, L i j =R i j y L i j ≠∅. Para todo j > 0, sea m = i j -i j-1 . Debido a las definiciones de ∆ 3 y ∆ 4 , para cada q m ∈ L i j , existe un estado q 0 ∈ L i j-1 y un segmento de ejecución q 0 ,...,q m de A en el segmento de palabra w (n+i j-1 ,n+i j ) tal que, para algún 0 < k ≤ m, q k ∈ F. Podemos organizar los segmentos de ejecución recopilados de esta manera mediante las siguientes definiciones.
Ahora, los segmentos de recorrido anteriores se unirán para formar un recorrido de aceptación infinito de A. Consideremos un árbol cuyo conjunto de nodos es ∪ j≥0 L i j × {j}. La raíz es (s,0) y el padre de un nodo (q,j) es ( predecesor (q,j), j-1). Este árbol es infinito, con ramificaciones finitas y completamente conectado. Por lo tanto, por el lema de König , existe un camino infinito (q 0 ,0),(q 1 ,1),(q 2 ,2),... en el árbol. Por lo tanto, lo que sigue es un recorrido de aceptación de A
Por lo tanto, por el principio del palomar infinito, w es aceptado por A.
Demostración: La definición de la función de proyección Pr puede extenderse de modo que en el segundo argumento pueda aceptar una palabra finita. Para algún conjunto de estados S, palabra finita w y símbolo a, sea Pr (S,aw) = Pr ( Pr (S,a),w) y Pr (S,ε) = S. Sea w ∈ L(A) y ρ=q 0 ,q 1 ,... una serie que acepta A sobre w . Primero, probaremos el siguiente lema útil.
En cualquier ejecución, A' solo puede hacer una elección no determinista una vez, es decir, cuando elige tomar una transición Δ 2 y el resto de la ejecución de A' es determinista. Sea n tal que satisfaga el lema 1. Hacemos que A' tome la transición Δ 2 en el paso n. Por lo tanto, definimos una ejecución ρ'=S 0 ,...,S n-1 ,({q n },∅),(L 1 ,R 1 ),(L 2 ,R 2 ),... de A' en la palabra w . Demostraremos que ρ' es una ejecución que acepta. L i ≠ ∅ porque hay una ejecución infinita de A que pasa por q n . Por lo tanto, solo nos queda demostrar que L i =R i ocurre infinitamente a menudo. Supongamos, por el contrario, que existe un índice m tal que, para todo i ≥ m, L i ≠R i . Sea j > m tal que q j+n ∈ F por lo tanto q j+n ∈ R j . Por el lema 1, existen k > j tales que L k = Pr({ q n },w(n,k+n)) = Pr({ q j+n },w(j+n,k+n)) ⊆ R k . Por lo tanto, L k =R k . Se ha derivado una contradicción. Por lo tanto, ρ' es una serie aceptante y w ∈ L(A').