@MASTERSTHESIS{ 2013:606787392,
 	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}
}