Dissertação
Model Checking Probabilistic Systems EVALUATED
Neste trabalho, apresentamos a implementação de uma ferramenta de verificação de modelos eficiente para fórmulas de uma lógica probabilística formal (EPPL) sobre circuitos digitais não fiáveis. Para aumentar a eficiência, capitalizamos em várias propriedades específicas destas estruturas; ainda assim, o programa mantém-se muito flexível, permitindo fácil adaptação a outros modelos mais complexos. Também é introduzido um método para minimizar problemas de espaço em verificadores de modelos sobre um subconjunto de sistemas probabilísticos representáveis por redes Bayesianas. Para tal, consideramos factorizações dos processos estocásticos associados aos espaços de probabilidades gerados pelos sistemas. São discutidas implicações de considerar uma extensão temporal sobre a lógica; é proposto um algoritmo de verificação para o caso temporal e são apresentadas opções de implementação.
março 26, 2009, 16:0
Publicação
Obra sujeita a Direitos de Autor
Orientação
