lunes, 12 de noviembre de 2012

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

martes, 6 de noviembre de 2012

Aplicaciones de Automatización y Control

Para esta semana nos toca investigar acerca de una aplicación que utiliza los conceptos aprendidos en clase, por lo que realizamos una búsqueda en google scholar en donde encontramos algún paper y explicarlo en esta entrada, por lo que yo estuve buscando algo relacionado con mi proyecto y exponer un breve resumen de lo leído  este es un paper llamado Active Noise Control System from Headphone Applications [1], escrito por Sen. M. Kuo, Sohini Mitra y Woon-Seng Gan.

En el paper que estuve leyendo vemos un diseño y una implementación de un sistema adaptativo en el cual podemos capturar el sonido exterior para crear un ambiente de menos sonido dentro de la capucha del audífono en donde se busca primero que nada el no utilizar mucho los recursos del micrófono que captura el ruido exterior y que también pueda predecir ese parámetro para crear una segunda fase en la cual se tiende que la señal del error tienda a 0.

Actualmente existen sistemas que utilizan una versión del Active Noise Control[2] en donde constantemente se captura el ruido y va comprando esa salida con lo que se genera de entrada para apegarse a que no exista más ruido exterior al que se tiene dentro de los audífonos  ellos consideran que este modelo no es lo suficientemente eficiente y por eso escriben ese paper para demostrar que sería mejor hacer ciertas modificaciones por el ejemplo el colocar de manera estratégica el micrófono para que solamente cada cierto tiempo de manera de entrada se capture ese dato y por medio de un procesamiento pueda ir adaptando de una mejor manera la señal de exaltación interior de la capucha, que en este caso utilizan música, aunque pudiera ser alguna otra cosa como audífonos especiales para ingeniería en donde se reciben comandos hablados[3] pero en el lugar donde se posicionan existe mucho ruido, llámese una planta o en alguna máquina, se necesita que el trabajador pueda escuchar estos comandos a pesar del ruido exterior.

Lo que hacen es tener una señal de referencia z que se captura de la fuente de ruido, para luego de esta entra a un procesado en donde procuran que la señal de control que altera el speaker interior de la capucha para producir un llamado antinoise que hace el aumento o disminución del audio producido, el micrófono por su parte mide el ruido residual y lo miniza por medio del procesamiento que genera al ANC al tratar de imitar o sintetizar la señal de referencia en lugar de utilizar el micrófono en si, si no que se tiene de una manera artificial ahorrando recursos y haciendo incluso el diseño de un ANC normal de manera más compacta, ya que los que se utilizan ellos nos dicen que tienen múltiples micrófonos, convirtiendo la señal digital a analógico de cada uno de ellos.

Por lo tanto, podemos decir que ellos en base a conceptos algoritmos adaptativos , ellos utilizan uno llamado FXLMS[4] que es el filtrado de la media cuadrada y poniendola como en una segunda forma de función de transferencia modelada para tomar los datos sintetizados del micrófono y generar la salida, también en base a la materia de control, ellos explican como diseñaron su sistema, al igual que uso de electrónica vista en materias de computo integrado.

Considero que este diseño que exponen es interesante, pero aunque se necesiten más recursos para estar captando y actualizando el ruido exterior resulte más costoso que de esta forma, creo que podemos tener un mejor audio interno actualizando a lo que está pasando en el exterior y no de una manera artificial, aunque ellos demuestren lo contrario.

Referencias.
[1] Active Noise Control System for Headphone Applications - Sen M. Kuo, Sohini Mitra -Liga
[2] Active Noise Control - Liga
[3] Electronic Hearing NoiseBuster - (Empresa que hace este tipo de audifonos) - Liga
[4] Algoritmo FXLMS - Liga

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 = E1F1 ω + ... + En Fn ω 

Donde E1, ... , En y F1, ... , Fn son expresiones regulares de ∑ y Λ∉L(Fi) para todas i.

Un lenguaje de G es:
L(G) = L(E1)L(F1)ω U ... U L(En)L(Fn)ω


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

jueves, 1 de noviembre de 2012

Lab 5: Factores cuadráticos

B.8.6 Dado
 Demuestre que:


Para poder demostrar estuve investigando como podemos decir que eso es correcto, por lo que primero que nada debemos de entender que la salida en estado estacionario de una función de transferencia de un sistema lo podemos obtener mediante la función de transferencia sinusoidal, esto quiere decir, que vamos a sustituir lo que es jωn en cada s que tenemos en nuestra función de transferencia, en donde la ω es la frecuencia , y la ωn es la frecuencia esquina para el factor cuadrático, ahora vamos a proceder con las formulas dadas.


Sustituimos
 Lo ponemos de modo que tengamos los factores cuadráticos en base a los 4 factores básicos que nos proponen en el libro, tenemos:


Por lo tanto, como sabemos, tenemos números complejos y partiendo de que cerca de la frecuencia ω = ω_n, hay un pico de resonancia, el factor de amortiguamiento relativo determina la magnitud de este pico, por lo tanto consideramos que son 1 y el numero complejo al cuadrado es -1, decimos que:

Por lo que hemos demostrado que:

Bibliografía.
[1] Chapter 8: Frecuency analysis, Modern Control Engineering, Fifth Edition, Katsuhiko Ogata.