Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM
Tesis (Lic. en Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2010.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | bachelorThesis |
| Language: | spa |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/40 |
| _version_ | 1801211449472712704 |
|---|---|
| author | Zandarin, Nicolás Hugo |
| author2 | D'Argenio, Pedro Ruben |
| author_facet | D'Argenio, Pedro Ruben Zandarin, Nicolás Hugo |
| author_sort | Zandarin, Nicolás Hugo |
| collection | Repositorio Digital Universitario |
| description | Tesis (Lic. en Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2010. |
| format | bachelorThesis |
| id | rdu-unc.40 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2011 |
| record_format | dspace |
| spelling | rdu-unc.402022-10-13T11:33:26Z Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM Zandarin, Nicolás Hugo D'Argenio, Pedro Ruben Software Program verification Model checking Métodos formales Explosión del espacio de estados Estados esenciales MTBDD PRISM Tesis (Lic. en Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2010. En este trabajo se presenta una adaptación al model checking simbólico de un método de reducción de estados, el cual, tiene como objetivo reducir el costo de los cálculos numéricos involucrados en el model checking probabilista. El método procede eligiendo estados distinguidos, que llamamos esenciales, como representantes de los estados que convergen con probabilidad 1 a tales estados. El espacio de estados se reduce, luego, al conjunto de estados esenciales y las transiciones se adaptan apropiadamente a esta reducción. También, se presenta una implementación del mismo sobre el model checker simbólico PRISM y los resultados obtenidos al verificar propiedades cuantitativas sobre diversos casos de estudio. 2011-09-05T19:32:52Z 2011-09-05T19:32:52Z 2010-12-17 bachelorThesis http://hdl.handle.net/11086/40 spa Atribución-NoComercial-SinDerivadas 2.5 Argentina http://creativecommons.org/licenses/by-nc-nd/2.5/ar/ 63 páginas |
| spellingShingle | Software Program verification Model checking Métodos formales Explosión del espacio de estados Estados esenciales MTBDD PRISM Zandarin, Nicolás Hugo Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM |
| title | Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM |
| title_full | Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM |
| title_fullStr | Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM |
| title_full_unstemmed | Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM |
| title_short | Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM |
| title_sort | abstraccion a estados esenciales en el model checker probabilista prism |
| topic | Software Program verification Model checking Métodos formales Explosión del espacio de estados Estados esenciales MTBDD PRISM |
| url | http://hdl.handle.net/11086/40 |
| work_keys_str_mv | AT zandarinnicolashugo abstraccionaestadosesencialesenelmodelcheckerprobabilistaprism |