Autómata Büchi No-Determinista

Verificación y Validación de Software
Entrada 10

Para esta semana se nos pidió hacer lo siguiente:

• Inventar una expresión ω-regular con por lo menos dos símbolos y por lo menos dos operadores.
• Dibujar el NBA que le corresponde.

Abecedario

$\sum {\left\{A, B, C\right\}}$

Expresión ω-regular

$(A^*B)(AC+C)^w$

Autómata Büchi No-Determinista

La siguiente imagen es un paso intermedio antes de llegar al autómata completo, aquí solo están las transiciones entre tres estados, donde tales transiciones son la separación por el AND de la expresión.

Y el autómata completo es el siguiente.

Entonces tenemos $L = \{Q, \sum, \delta, I, F\}$

Donde:
$Q = \{q0, q1, q2, q3\}$
$\sum = {\left\{A, B, C\right\}}$
$\delta$ son las transiciones mostradas en la imagen
$I = \{q0\}$
$F = \{q3\}$

Referencias:
Course On Principles Of Model Checking
Automata On Infinite Words