T12: Linear Temporal Logic

Como vimos en los ejemplos de maquina vending en clase, podemos formular la operación de recarga que se hace infinitas veces, debemos de satisfacer algunas propiedades, por lo que en base a esto realizamos desarrollamos el ejercicio.

Podemos ver que tenemos los siguientes operadores temporales y los conectivos:

Obtenida de LTS capítulo 14

Se nos pide formalizar la siguiente oración acerca de la maquina vending en LTL.

3) The recharge transaction occurs infinitely often.

Podemos expresar como T la operación de recarga, entonces, para decir que esta operación ocurre infinitamente utilizaremos los operadores temporales:

□   =    siempre

◇   =     eventualmente

Por lo tanto expresamos con T la operación de recarga,  para concluir que.

□◇T

Bibliografía
Capítulo 14 LTL Link

Tarea 10: expresión ω-regular & NBA

Para esta tarea tenemos que inventar una expresión regular ω y hacer el diagrama del automata no determinista de Büchi.

Una expresión ω-regular G en ∑ tiene la forma:

G = E₁F₁ ^ω + ... + E_n F_n ^ω 

Donde E₁, ... , E_n y F₁, ... , F_n son expresiones regulares de ∑ y Λ∉L(Fi) para todas i.

Un lenguaje de G es:

L(G) = L(E₁)L(F₁)^ω U ... U L(E_n)L(F_n)^ω

Por lo tanto, pongo la siguiente expresión.

(A+B)+(AB)^ω

 

 Este sería mi NBA.

 Bibliografía.

• Concurrency - Slides - Link
• Principles of Model Checking - Christel Baier - Link
• Automata - Berndt Farwe - Link

Tarea 9: Grafo de programa

Para esta entrada de verificación voy a hacer un sistema en donde podamos modelar en base al reciclaje del papel, por lo que podemos decir que  el sistema consta de los siguientes procesos.

• Recolectar papel y Clasificar el papel(Recolección)
• Se moja y se bate para crear pasta (Creación_pasta)
• Se limpia la pasta de pegamento, tintes, etc. (Limpieza)
• Se moldea en superficia plana. (Molde_pasta)
• Secado y enrollado de hoja. (Generar_papel)

Entonces, podemos tener un sistema en donde por ejemplo, ya tenmos papel previamente limpiado, o ya tenemos la pasta, y se pueden automatizar los procesos ya que según el estado en el que tengamos el papel, vamos a utilizar las herramientas que tengamos, por lo que considero que estos serian los procesos fundamentales en donde los procesos tienen solamente dos estados llamados 0 y 1.

Ahora, en base a estos procedimiento, voy a crear el sistema en base al estado del papel en donde según el estado, vamos a crear las transiciones del sistema dado el siguiente diagrama.

En donde el sistema global inicial es 0000, pero para poder iniciar el ciclo necesitamos por lo menos tener papel, por lo que pongo como estado global el tener papel recolectado 1000.

Bibliografia.
Principles of Model Cheking, Baier & Katoen,

Red Petri

La red petri son los tipos de modelos que se utilizaron en sistemas distribuidos, utilizan tokens que van viajando dentro de los estados, sirve para investigar las combinaciones de tokens permitidas en posiciones en las cuales no son permitidas.

Para esta tarea hice una red petri sencilla en donde modele un sistema de reconocimiento de huellas, como el que se utilizan en las empresas, para abrir o cerrar una puerta.

El aparato siempre esta en la espera de que entre un dedo, al momento de que ponga el dedo empieza a capturar su huella digital, después el sistema empieza a reconocerlo y decide si se abre o no la puerta, por lo que podemos decir que tenemos entonces los siguientes estados.

• Esperando.
• Capturando.
• Reconociendo.
• Abierto
• Cerrado.

Incluyendo 5 transiciones diferentes y el token sería el dedo o la huella.

Utilizando python realizamos un modelo.


Teniendo como resultado el siguiente diagrama.

Esta sería me entrada de validación, para más información sobre las redes petri, pueden ver información en el wiki aquí.

La lógica predicativa en las bases de datos.

Como pudimos ver en clase de verificación de software, la lógica predicativa tiene una alta gama de significaciones que la lógica booleana que hemos visto anteriormente, por lo que este tipo de lógica predicativa tiene aplicaciones más diversas, para esta entrada voy a explicar como podemos utilizar la lógica predicativa en las bases de datos.

Primero que nada vamos a definir base de datos, la cual podemos decir que es una colección finita de datos relacionados, por ejemplo un diccionario inglés-español, un directorio de teléfonos, etc...

En una base de datos podemos encontrar los siguientes elementos los cuales podemos representarlos de manera lógica [1]:

• Un átomo = numero, letra, etc...
• Representado en lógica como un elemento en el universo.

• Un registro = una tupla de elementos atómicos.
• Representado en lógica como un hecho.

• Una tabla = una colección de registros compatibles.
• Representado en lógica como una relación.

• Una base de datos relacionada = una colección de tablas
• Representado en lógica como una colección de relaciones

• Una base de datos deductiva = base de datos relacionada incluyendo mecanismos deductivos.
• Representado en lógica como una base de datos extensional y bases de datos intencionales (esto quiere decir que se incluyen ciertas reglas)

• Un query = es una herramienta linguistica para seleccionar información.
• Representado en lógica como una fórmula.

Entonces podemos decir que el modelo de bases de datos deductivo es una restricción de primer orden de la lógica de predicativa en un modelo de datos relacional, este modelo deductivo se hacen relaciones bien definidos extensionalmente a través de hechos o intencionalmente a través de reglas, en donde las reglas pueden ser definidas, como podemos ver en la arquitectura de una base de datos deductiva.

Arquitectura de una base de datos deductiva

Podemos decir que las bases de datos extensionales, las restrucciones de integridad y las queries están presentes en los sistemas tradicionales de bases de datos, lo que se diferencia la base de datos deductivas es que ofrece almacenar reglas deductivas en bases de datos intensionales y proporcionar un mecanismo de deducción.

Se han desarrollado varios lenguajes formales para este tipo de modelo de datos deductiva, por ejemplo existe un lenguaje llamado Datalog [2], un sublenguaje en donde se le llena una base de datos y se ingresan algún query que cumple con lógica predicativa de primer ornen, también lenguajes como Prolog [3], extienden las estructuras de bases de datos complejas utilizando componentes en donde se combinan el lenguaje lógico declarativo con el almacenamiento de datos en base a sus datos y las reglas.

Los hechos en datalog son representados en forma de relaciones NOMBRE(argumento-1, ..... argument-n), donde NOMBRE es el nombre de la relación y argumento son las constantes.

Por ejemplo, DIRECCION(Roberto, 'Calle 13')

Los queries atómicas son representados de la siguiente forma: NOMBRE(argumento-1.... argumento-n), donde los argumentos son constantes o variables que incluyen la variable ''-" negación.

Las reglas en datalog son expresadas de la siguiente forma.

En donde las Z son vectores de variables o constantes en donde cualquier variable que aparece en la parte de la izquierda de ":-" aparece también del lado derecho.

La semántica en datalog es la forma:

En donde todas las variables que aparecen tanto de lado izquierdo como de lado derecho de la regla (llamados cabeza y cuerpo) son universalmente cuantificados, mientras que los que solamente aparecen de lado izquierdo (en el cuerpo) están existencialmente cuantificados.

Entonces en base a los conceptos anteriores voy a desarrollar un ejemplo en donde vamos a utilizar lo anterior, supongamos que necesitamos realizar una base de datos que contenga información acerca de autores de libros, vamos a guardar en una relación, llamada AUTOR y otra relación llamada TITULO de la siguiente manera:

• AUTOR(Nombre_autor, Id) 
• Esto significa que el autor cuyo nombre tiene una identificación ID
• TITULO(Id, Nombre_libro)
• Esto significa que el autor cuyo numero de ID es autor o coautor de un libro titulado Nombre_libro.

Ahora por ejemplo vamos a definir una nueva relación COAUTOR(Nombre_1, Nombre_2), el cual significa que dichos nombres fueron coautores del libro:

COAUTOR(Nombre_1, Nombre_2) :- AUTOR(Nombre_1, ID_1), TITULO(ID_1, Nombre_libro), AUTOR(Nombre_2, ID_2), TITULO(ID_2, Nombre_libro), Nombre_1 =/= Nombre_2.

Podemos ver que la regla que hemos realizado diciendo que tenemos un número de ID único en donde a esta variable le podemos decir que es una restricción de integridad que cumple con la siguiente semántica:

Entonces este sería una forma de modelar una base de datos por medio del lenguaje Datalog, se puede implementar este tipo de bases en nuestros programas incluyendo la lógica en base a algunas extensiones por ejemplo en python existe pyDatalog [4] en donde de manera sencilla podemos modelar una base de datos deductiva.

Esta sería mi tarea de verificación si tienen alguna duda espero me lo hagan saber.

Bibliografía.

[1] Lectura de la clase lógica de la Universidad de Linkoping liga.

[2] Lenguaje Datalog liga

[3] GNU Prolog website. liga

[4] pyDatalog liga

Ejercicio tarea 6

En base al capítulo 4 del libro "The world according to predicate logic" he seleccionado un ejercicio para repasar lo que vimos en la materia de verificación y validación de software, en donde habla con detalle sobre los cuantificadores, en donde para entender el tema se nos proporcionan los siguientes ejemplos en la página 4-7.

• Alguien camina
• ∃xWx

• Algún chico camina
• ∃x(Bx∧Wx)

• Un chico camina
• ∃x(Bx∧Wx)

• Jose mira a una chica
• ∃x(Gx∧Sjx)

• Una chica mira a Jose
• ∃x(Gx∧Sxj)

• Una chica mira se mira
• ∃x(Gx∧Sxx)

Como podemos ver lo que cada variable hace según la oración, pero en los ejemplos anteriores solamente estamos viendo los cuantificadores de uno solo en el cual utilizamos el simbolo ∃ que se utiliza para algo existente, si queremos abarcar a todos, nos encontramos con el simbolo ∀ el cual es un cuantificador universal, podemos ver los siguientes ejemplos:

• Todos caminan
• ∀xWx

• Cada chico caminan
• ∀x(Bx⇒Wx)

• Cada chica mira a María
• ∀x(Gx⇒Sxm)

Hay que tener en cuenta que "Un chico camina" se traduce con un simbolo de conjunción y "Cada chico camina" se translada usando el simbolo de implicación, entonces la idea de este ejercicio es expresar por medio de predicados.

Sea B el predicado de "chico" y W es "caminar".

a) ¿Qué expresa la siguiente expresión: ∀x(Bx∧Wx) ?

b) ¿Qué expresa la siguiente expresión: ∃x(Bx⇒Wx) ?

Al principio, estas expresiones se me hicieron un poco extrañas, pero reflexionando sobre esto y llegando un poco más profundo viendo el significado y la estructura de los objetos.

Voy a empezar con el inciso a.

Teniendo la expresión ∀x(Bx∧Wx) podemos decir que literalmente lo podemos traducir como: "Todo x tiene las cualidades B y W" entonces lo podemos expresar de la siguiente manera "Todo aquel que es un chico y camina"

Respuesta:

∀x(Bx∧Wx)
Todo x tiene las cualidades B y W
Todo aquel que es un chico y camina

Ahora para el inciso b.

Teniendo la expresión ∃x(Bx⇒Wx) podemos decir que literalmente lo podemos traducir como: "Existe una x tal que si es B, entonces tiene la cualidad W" entonces lo podemos expresar de la siguiente manera: "Existe alguien que camina, si es chico"

Respuesta:

∃x(Bx⇒Wx)
Existe una x tal que si es B, entonces tiene la cualidad W
Existe alguien que camina, si es chico

Como ven lo que hice es primero en base a la estructura de los objetos sacar una oración que se pueda expresar con sus cualidades y luego traducirla de manera que podamos tener una expresión.

Lógica predicativa

En base al libro: "Lean Symbolic Logic", que vimos en la clase de validación de software, desarrollo el siguiente ejercicio:

• "All my cousins are unjust"
• "No judges are unjust"

Traducción al español:

• "Todos mis primos son injustos"
• "Ningún juez es injusto"

Ahora utilizo las siguientes expresiones para cada una.

• C(x): Mis primos
• J(x): Juez
• U(x): Injusto

En base a la primera oración tenemos la siguiente expresión.

• "Todos mis primos son injustos"
• ∀x C(x) ⇒ U(x)

En base a la primera oración tenemos la siguiente expresión.

• "Ningún juez es injusto"
• ¬∃x J(x) ⇒ U(x)

Por lo tanto podemos decir que 

• "Ninguno de mis primos es juez"
• ∴  ¬∃C(x)⇒J(x)

Formulando las siguientes expresiones de las oraciones:

∀x C(x) ⇒ U(x)

¬∃x J(x) ⇒ U(x)

∴  ¬∃C(x)⇒J(x)

BDD

Primero que nada, inventé una expresión con las características deseadas que nos dice en la presentación, por lo que podemos ver que tiene los conectivos y las 3 variables.

Expresión:

((A ^ B)  ^ (B  ^ A)) v ¬ C )

Ahora tenemos el BDD, el cual contiene la expresión hecha en un diagrama binario de desición, tal como lo muestra en el PDF aqui. este es el resultado.

BDD:

Como podemos ver, este diagrama se puede reducir, si se fijan, tenemos salidas repetidas en los primeros 6 nodos de izquierda a derecha, tenemos 1 y 0, por lo que facilmente podemos reducirlo y obtener algo como el siguiente diagrama.

ROBDD:

En este diagrama reducido podemos ver que los 3 nodos repetidos se juntan en C, siguiendo los pasos descritos en el libro podemos decir que este es un ROBDD del primero BDD.

Saludos :)

Aplicación de la lógica proposicional.

Introducción.

Para la tercera tarea de la materia de verificación y validación de software se nos pide investigar aplicaciones de la lógica proposicional y documentar uno.

Una de las formas de definir la lógica proposicional, como lo vimos en la materia, es el estudio de las formas de razonamiento donde su validación depende solamente de las propiedades verdadero o falso, es el primer paso para la definición de lo que es la lógica y el razonamiento en sí,  como por ejemplo, la siguiente proposición "si llueve, llevo mi paraguas": Llueve -> Paraguas.

El lenguaje natural y la lógica proposicional

La lógica proposicional se puede utilizar para razonar diferentes argumentos del lenguaje natural[1], podemos hacer una serie de pasos para determinar primero que nada las premisas y la conclusión de un argumento identificando las proposiciones formales, luego la lógica proposicional se emplea para determinar si la conclusión es valida según esas premisas, ahora les muestro un ejemplo, supongamos que tenemos la siguiente canción de Joan Manuel Serrat, en donde tenemos el siguiente párrafo.

Caminante son tus huellas el camino y nada más.
Caminante no hay camino, se hace camino al andar,
Al andar se hace camino y al volver la vista hacia atrás.
Se ve la senda que nunca se ha de volver a pisar.
Caminante no hay camino, hay estelas en el mar.

Entonces para poder estudiar el lenguaje natural debemos de seguir una serie de pasos [2]:

• a) Identificar los enunciados simples: importante recalcar que solamente se formaliza las oraciones declarativas, o sea las que afirman o niegan, fijandose que hablen del mismo objeto, desechandonos de información irrelevante
• b) Asignar a cada enunciado simple una constante proposicional.
• d) Identificar las conectivas lógicas: verificar las conectivas no, y, o, si, si y sólo si, algunas veces algunas otras cumplen con la función, como es el caso de la coma.
• d) Reconstruir los enunciados complejos a partir de los simples y de las conectivas.

Ahora, podemos estudiar este párrafo y encontrar los conectores para demostrar si la conclusión que esta persona que escribió este autor es verdadera, hacemos los siguiente.

Caminante son tus huellas el camino y nada más.
Caminante no hay camino, se hace camino al andar,
Al andar se hace camino y al volver la vista hacia atrás.
Se ve la senda que nunca se ha de volver a pisar.
Caminante no hay camino, hay estelas en el mar.

Los conectivos tienen una traducción en la lógica proposicional, como podemos ver en la siguiente tabla, podemos separar estas proposiciones.

Símbolo	Lógica	Representación
->	Implicación	coma
^	AND	y
v	OR	o
¬	Negación	no

Ahora vamos a representar las siguientes proposiciones.

• p: Caminante son tus huellas el camino
• q: Caminante son tus huellas nada más
• v: Caminante hay camino
• s: Caminante se hace camino al andar
• t: Caminante al volver la vista atrás
• y: Caminante se ve la senda que se ha de volver a pisar.
• v: Caminante hay estelas en el mar.

Ahora podemos hacer una definición formal de este párrafo.

((( p ^ q ) -> ¬ r) -> s ) -> ( s ^ t ) -> ¬ y -> ¬r -> v

Ahora con el script[3] que hacia realizado anteriormente, lo modifiqué para sacar una tabla de verdad y cuando todas son verdaderas, la definición formal arroja verdadero, cuando todas son falsas arroja que es falsa, por lo que podemos concluir que esta proposición es verdadera y tiene coherencia.

Con esto, tiene su aplicación al examinar la sintaxis y la semántica tanto de la lógica como del lenguaje natural, como lo podemos ver en el documento [4] de la Universidad de Missouri, donde utilizan lenguaje lógico proposicional para procesar el lenguaje natural, creando una relación estrecha por medio de gráfos, en donde cada nodo se representa por una conectiva y por preposiciones, y las relaciones entre ambas.

La lógica proposicional en la industria.

La lógica proposicional es de suma importancia en la industria, sobre todo en sistemas computacionales formales e inteligentes, ya que esta sienta las bases para poder tener fundamentos teóricos y formales para el modelado de sistemas al igual que el tratamiento inteligente de datos para una solución tecnológica.

En psicología, por ejemplo, la cognitiva del ser humano hace énfasis en que tenemos cada uno de nosotros una complejidad en cuestión del aprendizaje por lo que se concluye que nosotros representamos el contenido por estados mentales y representaciones, por ejemplo Newell y Simon [5] en 1972 realizaron un estudio sobre el aprendizaje modelando la mente humana como un sistema de procesamiento de información, planteando que el pensamiento es el hecho de procesar mucha información manipulando símbolos, entonces los estados mentales del ser humano se empezaron a comprar con sistemas de signos organizados en un lenguaje en donde se deben de conocer las reglas, en este caso estas reglas utilizan la lógica proposicional para describir las representaciones mentales.

Todo esto nos lleva a que la lógica proposicional ayuda de una forma matemática a aplicar computacionalmente representaciones mentales y obtener inteligencia la cual no proviene de un ser humano, si no que, es artificial dentro de una computadora, es aquí en donde la lógica proposicional tiene cabida, con el hecho de que muchas aplicaciones con lo que actualmente interactuámos, tiene inteligencia artificial, el hecho de jugar un videojuego con la computadora hace que estemos relacionándonos con una inteligencia que no es de un ser.

Espero que esta tarea ayude a comprender la importancia de la lógica proposicional.

Bibliografía

[1] Applications of Propositional Calculus, Mathematical Approaches to Software Quality, Gerard O' Regan, Springer.

[2] La formalización del lenguaje natural, Universidad de Granda

[3] Tarea de tautología: liga
[4] A logical Language for Natural Language Processing, Syed S. Ali

[5] L'apprentissage organisationnel, Frédéric LEROY liga

Ejemplo de Tautología.

El script es solo para hacer la tabla y verificar si es una tautología

Introducción a la validación y verificación de software

Como una pequeña introducción para la materia, estuve investigando sobre la validación y verificación de software para así comprender para que sirven estos métodos formales y en el futuro comprenderlos para implementarlos en sistemas que lo requieran.

Para empezar, podemos decir que la validación de software es el saber si nuestro sistema hace lo que nosotros buscamos que haga, esto quiere decir que si construimos el sistema de manera correcta, no es simplemente ver el código, si no que existen métodos formales que tiene cierta dificultad para determinar si se hace lo correcto, según lo que el usuario o el cliente en realidad necesita o requiere, podemos decir que contesta a la pregunta ¿Estamos haciendo el sistema correcto? [1].


Por otra parte, podemos decir que la verificación de software es saber si el sistema que estamos desarrollando hace de manera funcional y no funcional lo que nosotros especificamos en algún análisis previo a implementarlo y compararlo utilizando métodos formales, podemos decir que contesta a la pregunta ¿Estamos haciendo el sistema correctamente? [1].

Por lo tanto, podemos decir que cuando nosotros tenemos un sistema, por ejemplo, que involucre conceptos de sistemas distribuidos, paralelos, necesitemos entradas o salidas de sensores, no existe una manera sencilla de saber que todas las combinaciones posibles funcionen correctamente dependiendo de los eventos ocurridos, la unica manera de poder realizar esto es con métodos formales, expresando toda la especificación del sistema en un lenguaje matemático lógico, examinando que no existan cuestiones en el sistema que no deberían de pasar, esto quiere decir que no vamos a correr el sistema en sí, si no que se va  estudiar con estos métodos para saber si la especificación es correcta.

Es importante recalcar que nunca vamos a tener un sistema el cual no tenga errores o defectos, pero este tipo de métodos nos sirven para reducir el porcentaje de defectos y tener un producto mejor al momento de usarlo.

En conjunto, podemos utilizar la validación y la verifiación del software como un proceso para analizar si el sistema en desarrollo o final, cumple con los requisitos del cliente y se encuentra conforme con la especificación del mismo.

Buscando en la web, encontré algunas empresas en México que se dedican o manejan como alguno de sus servicios la verificación y validación de software, entre ellas se encuentran: IRQA, DNV, Epicor, entre otras.

La razón por la que esta materia es importante es que estudios como por ejemplo de la empresa Compuware, en donde revela que después de un análisis, las empresas que tienen un fallo por medio de software alcanzan hasta los 7.5 millones de euros en una hora [2], este sector, incluyendo por ejemplo a los trabajadores sin actividad de hasta 140 horas anuales o suspension de total de ventas.

Por listar algunos errores de software [3] que se pudieron haber evitado con una buena implementación de validación y verificación son:

• Un error en el código de control del producto Therac-25 fue la responsable de al menos 5 muertes en la decada de los 80, produciendo cantidades exageradas de rayos X [4].

• El Ariane 5 fue destruido 40 segundos después del despegue debido a un error de software a borde, causando perdidas de millones de dólares [5].

• El error de software de MIM-104 Patriot hacia que su reloj del sistema estuviera a la deriva en un tercio de segundo, llevando al fracaso el interceptar un misil [6].

Bibliografía

[1]  Software Engineering: A Practitioner’s Approach, 7/e  (McGraw-Hill 2009).
[2]  Los fallos informáticos suponen pérdidas, Computing.es (2012) Liga.
[3]  List of software bugs, Wikipedia Liga.
[4]  An investigation of the Therac-25 Accidents, Nancy Leveson, University of Washington (1993) Liga
[5]  ARIANE 5 Report, Inquiry Board (1996) Liga.
[6]  Patriot Missile Software Failure, Aly Farahat, Slides (2009) Liga.

Verificación

Roberto