@MASTERSTHESIS{ 2013:727615012,
 	title = {Tradu??o de modelos de redes de automatos estoc?sticos para a linguagem do NUSMV},
 	year = {2013},
 	url = "http://tede2.pucrs.br/tede2/handle/tede/5260",
 	abstract = "Redes de aut?matos estoc?sticos (SAN) ? um formalismo que permite a descri??o de sistemas a fim de realizar avalia??es quantitativas. O objetivo deste trabalho ? possibilitar avalia??es qualitativas de modelos SAN atrav?s de sua tradu??o para a linguagem de um verificador existente. O trabalho prop?e, detalha e exemplifica o mapeamento de um subconjunto de modelos SAN para a linguagem de entrada do NuSMV. Conforme o resultado observado, os modelos para o NuSMV gerados pelo tradutor preservam a sem?ntica dos respectivos modelos SAN originais pois apresentam sistemas de transi??o de estados isom?rficos. A verifica??o de propriedades em CTL (Computation Tree Logic) sobre os modelos SAN ? exemplificada",
 	publisher = {Pontif?cia Universidade Cat?lica do Rio Grande do Sul},
 	scholl = {Programa de P?s-Gradua??o em Ci?ncia da Computa??o},
 	note = {Faculdade de Inform?ca}
}