martes, 13 de noviembre de 2012

Tarea 11

Logica Temporal Lineal:
La lógica temporal es una extensión de la lógica modal, la cual es prácticamente usada en sistema de reglas, donde esta presente el tiempo.Wikipedia

Connectives and Temporal Operators


Como ejemplo tomaré los enunciados:

1.-At some point, i will hold forever
Solucion


2.-If a student forgets a coin in the coin slot, she (or another student) will use this coin to get a drink before any professor can do this.
Solucion:
(sfc(¬pct R eac))
sfc : student forgets a coin
eac: Student uses coin
pct :professor uses coin

Referencias:
Enlace 1
Enlace 2

sábado, 3 de noviembre de 2012

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