Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial
Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2010.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | doctoralThesis |
| Language: | spa |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/136 |
| _version_ | 1801212214027223040 |
|---|---|
| author | Giro, Sergio Sebastián |
| author2 | D'Argenio, Pedro Ruben |
| author_facet | D'Argenio, Pedro Ruben Giro, Sergio Sebastián |
| author_sort | Giro, Sergio Sebastián |
| collection | Repositorio Digital Universitario |
| description | Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2010. |
| format | doctoralThesis |
| id | rdu-unc.136 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2011 |
| record_format | dspace |
| spelling | rdu-unc.1362023-08-31T19:07:44Z Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial Giro, Sergio Sebastián D'Argenio, Pedro Ruben Performance analysis and design aids Performance of systems Análisis de ejecución y ayudas de diseño Ejecución de los sistemas Sistemas distribuidos Tesis (Doctor en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2010. En esta tesis desarrollamos algoritmos y técnicas de análisis basadas en model checking para analizar la corrección de sistemas distribuidos con características aleatorias y no deterministas. Una contribución importante es la demostración de que no existe un algoritmo que resuelva el problema de verificación de forma totalmente automática. A pesar de este resultado, presentamos algoritmos que, si bien no pueden determinar la corrección para todos los sistemas y propiedades, sirven para detectar que ciertos sistemas son correctos o incorrectos. Uno de los impedimentos más frecuentes a la hora de verificar PDMs es el problema de la explosión de estado. Este problema, bien conocido y atacado en model checking, se agrava en el ámbito de model checking cuantitativo. Existen trabajos previos que, con el fin de atacar este problema, presentan adaptaciones de las técnicas de reducción orden parcial para model checking cualitativo al caso cuantitativo. Presentamos una nueva adaptación de la técnica de reducción de orden parcial. Nuestra adaptación aprovecha el hecho de que las componentes de un sistema concurrente tienen acceso limitado a la información sobre el estado global del sistema. Concluímos con casos de estudio que muestran las mejoras de nuestros algoritmos y nuestra técnica de orden parcial. 2011-09-06T15:27:13Z 2011-09-06T15:27:13Z 2010-03 doctoralThesis http://hdl.handle.net/11086/136 spa Atribución-NoComercial-SinDerivadas 2.5 Argentina http://creativecommons.org/licenses/by-nc-nd/2.5/ar/ 224 páginas |
| spellingShingle | Performance analysis and design aids Performance of systems Análisis de ejecución y ayudas de diseño Ejecución de los sistemas Sistemas distribuidos Giro, Sergio Sebastián Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial |
| title | Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial |
| title_full | Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial |
| title_fullStr | Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial |
| title_full_unstemmed | Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial |
| title_short | Sobre la verificación automática de autómatas probabilistas distribuidos con información parcial |
| title_sort | sobre la verificacion automatica de automatas probabilistas distribuidos con informacion parcial |
| topic | Performance analysis and design aids Performance of systems Análisis de ejecución y ayudas de diseño Ejecución de los sistemas Sistemas distribuidos |
| url | http://hdl.handle.net/11086/136 |
| work_keys_str_mv | AT girosergiosebastian sobrelaverificacionautomaticadeautomatasprobabilistasdistribuidosconinformacionparcial |