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.
Sistemas probabilísticos, verificação de modelos, circuitos digitais, lógica temporal, lógica probabilística

Março 26, 2009, 16:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Paulo Alexandre Carreira Mateus

Departamento de Matemática (DM)

Professor Auxiliar