@MASTERSTHESIS{ 2013:1328214132, title = {Gera??o de contraexemplos e testemunhas para um verificador de modelos descritos em redes de aut?matos estoc?sticos}, year = {2013}, url = "http://tede2.pucrs.br/tede2/handle/tede/5225", abstract = "A possibilidade de gera??o de contraexemplos e testemunhas ? um dos principais atrativos da t?cnica de Verifica??o de Modelos. Os contraexemplos s?o uma boa fonte para depura??o do sistema, pois s?o gerados quando uma especifica??o ? refutada pelo modelo. J? as testemunhas ratificam a satisfa??o de uma especifica??o pelo modelo atrav?s de uma execu??o do sistema. Esta disserta??o de Mestrado ? parte de um projeto de constru??o de um verificador de modelos para modelos descritos em Redes de Aut?matos Estoc?sticos e trata da implementa??o da gera??o de contraexemplos e testemunhas para a ferramenta", 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} }