[VVS] 10. Propiedades de modelos de verificación

La tarea de esta semana consistió en lo siguiente:

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

Un Autómata Büchi no determinista es una quintupla A = (Q, Σ, Q0, δ, F) sobre un abecedario Σ, donde:

• Q es un conjunto finito de estados
• Q0 ⊆ Q es un conjunto no vacío de estados iniciales
• δ : Q × Σ → 2^Q es una función de transición
• F ⊆ Q es un conjunto de estados finales.

Los operadores de un Autómata Büchi no determinista están definidos en la siguiente tabla

Operador	Símbolo	Representación
Unión	L1 ∪ L2 L1 + L2
Concatenación	L1 • L2 (L1)(L2)
Clausura	L1*

Para el ejemplo que tomaré, el abecedario estará dado por:

Σ = {a, b, c}

Y la expresión ω-regular será:

ab*+c

Podemos representar la expresión anterior construyendo el autómata paso a paso, primero la unión:

Despues dividimos la concatenación y resolvemos:

Por último la clausura, así obtenemos el autómata final.

Solo para complementar la información:

• Q = {q0, q1, q2, q3, q4, q5}
• Q0 = {q0}
• F = {q4}
• Σ = {a, b, c}

REFERENCIAS

• http://webdelprofesor.ula.ve/ingenieria/hyelitza/materias/preteoria/apuntes/tema2.pdf
• http://web.ing.puc.cl/~marenas/iic3800/clases/automata-1-imp.pdf
• [Libro] Principles of Model Checking - Christer Baier & Joost-Pieter Katoen