Tarea 10 Propiedades de modelos de verificacion

Para esta semana se nos pide Inventar una expresion w-regular y crear un NBA(Non-deterministic Buchi Automata)

En ciencias de la computación y la teoría de autómatas , un autómata Büchi es un tipo de autómata , que se extiende un autómata finito a los insumos infinitas. Acepta una infinita secuencia de entrada si y sólo si existe una ejecución del autómata que visita (al menos) uno de los estados finales infinitas veces. 

• Contener por lo menos 2 Simbolos
• Contener por lo menos 2 operadores

Solucion:

Expresion:

Representacion NBA :

Donde

Q = {q0.q1,q2,q3} Conjunto de Estados

S={q0} Estado Inicial

F={q0,q1,q3}Estados Finales

Σ = {a,b} Alfabeto de Entrada

Nota:
* Es para encontrar algo que se encuentra repetido 0 o mas veces
+ se encuentra repetido 1 o mas veces
.  cualquier caracter individual solo el salto de linea

Referencias:
http://web.ing.puc.cl/~marenas/iic3800/clases/automata-1-imp.pdf