Automatización del análisis del tiempo de ejecución de programas probabilísticos

Abstract

Los programas probabilísticos son un tópico relevante en la computación moderna, por lo tanto, razonar sobre su tiempo de ejecución asociado es un objetivo de alto interés, tanto en lo teórico como en lo práctico. Uno de los enfoques existentes para abortar esto último es la técnica de la transformada ert[·]. Esta transformada es una función recursiva sobre el conjunto de programas probabilísticos que permite calcular el tiempo de ejecución esperado de un programa dado. Si bien, la transformada ert[·] posee suficiente expresividad para calcular de forma precisa el tiempo de ejecución de un programa, debido a su definición, posee algunos inconvenientes para ser utilizada en la práctica. El principal inconveniente es la elevada cantidad de cálculos necesarios para obtener un tiempo de ejecución válido. Otro inconveniente asociado es el cálculo del tiempo de ejecución de un ciclo while; esto requiere comprobar una desigualdad entre funciones. Este proceso no posee una metodología clara para llevarse a cabo y, en general, se resuelve mediante la manipulación algebraica de expresiones. El objetivo general de este trabajo es desarrollar una herramienta que permita calcular, de forma automática, el tiempo de ejecución de un programa probabilístico, usando la transformada ert[·]. Para lograr esto, se procedió a implementar la función ert[·] y algunas estructuras asociadas en el lenguaje Haskell. Luego, a través de una herramienta denominada como smt-solver, se procedió a comprobar la condición asociada a los ciclos while. Para comprobar el desempeño de la herramienta desarrollada se diseñaron tests que permitieron comparar los resultados manuales con los cálculos automatizados. La herramienta logra reproducir los cálculos manuales para cada test desarrollado, por lo tanto, se concluye que el resultado final es positivo. Dado esto, es posible afirmar que el trabajo desarrollado es un primer acercamiento para que en un futuro la técnica ert[·] pueda ser utilizada en la práctica.