Imagen de cubierta local
Imagen de cubierta local
Imagen de Google Jackets

Abstracción a estados esenciales en el Model Checker Probabilista PRISM / Nicolás H. Zandarin.

Por: Colaborador(es): Detalles de publicación: [S.l. : s.n. ], 2010.Descripción: 63 páginas : ilustraciones ; 30 cmTema(s): Recursos en línea: Nota de disertación: Tesis (Lic. en Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2010. Resumen: 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.
Etiquetas de esta biblioteca: No hay etiquetas de esta biblioteca para este título.
Existencias
Tipo de ítem Biblioteca actual Signatura Copia número Estado Notas Fecha de vencimiento Código de barras Reserva de ítems
Trabajo Especial de Grado Trabajo Especial de Grado FaMAF Secc. Tesis y Trabajos especiales Trabajo Especial Computación CAJA 11 - 20760 1 Disponible 20760
Trabajo Especial de Grado Trabajo Especial de Grado FaMAF Depósito Interno TE C ZAN ej.2 2 Disponible Disponible también en línea 20761
Total de reservas: 0

Tesis (Lic. en Computación)--Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física, 2010.

Bibliografía : p. 61-63.

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.

Haga clic en una imagen para verla en el visor de imágenes

Imagen de cubierta local


Nuestras Redes Sociales

facebook Instagram

Horario de la Biblioteca: lunes a viernes de 8:30 a 18:30hs

Av. Medina Allende s/n , Ciudad Universitaria, Córdoba, Argentina

Tel: +54 351 5353701 int. 41127 (Atención al Público) int. 41151 (Dirección)

biblio@famaf.unc.edu.ar (Dirección)

publicofamaf@gmail.com (Atención al público)