Abstracción a Estados Esenciales en el Model Checker Probabilista PRISM
Ver/Descargar
Fecha
2010-12-17Autor
Zandarin, Nicolás Hugo
Director/a
D'Argenio, Pedro Ruben
Metadatos
Mostrar el registro completo del ítemResumen
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.