T16 - Verificação de modelos probabilísticos

20 dezembro 2012, 15:00 • David João Barros Henriques

Verificação simbólica de modelos probabilísticos. Diagramas de decisão multi terminal. Representação simbólica de matrizes e vectores reais, operações eficientes com MTBDDs. A linguagem de modelação e verificação PRISM. Módulos, comandos, sincronização, exemplos. Especificação e verificação de propriedades PCTL em PRISM. Resolução de exercícios de exames anteriores.

T15 - Verificação de modelos probabilísticos

17 dezembro 2012, 09:00 • David João Barros Henriques

Verificação eficiente de propriedades PCTL em cadeias de Markov. Modelos probabilísticos não determinísticos. Processos de decisão de Markov. Sistema de transição induzido por um processo de decisão de Markov. Adversários. Cadeia de Markov induzida por um adversário. CTL  probabilístico para MDPs: sintaxe e semântica. Adversários sem memória. Suficiência de adversários sem memória. Verificação eficiente de propriedades de alcance. Caracterizações de propriedades por menor ponto fixo. Método de iteração de valores para Verificação eficiente de propriedades PCTL em processos de decisão de Markov. Exercícios.

T14 - Verificação de modelos probabilísticos

13 dezembro 2012, 15:00 • David João Barros Henriques

Modelos probabilísticos. Cadeias de Markov. Sistema de transição induzido por uma cadeia de Markov. Conceitos básicos de teoria da probabilidade. Conjuntos de cilindros. Sigma-algebra induzida por cilindros. CTL probabilístico: sintaxe e semântica. Mensurabilidade de fórmulas PCTL. Verificação eficiente de propriedades de alcance. Caracterizações de propriedades por menor ponto fixo. Exercícios.

P11 - SVM e ROBDDs

10 dezembro 2012, 09:00 • David João Barros Henriques

Apresentação do software de verificação SVM. Tipos de dados, Sincronização, Modulos, comandos Assign vs Define, Especificação de propriedades CTL, Composição, Justiça.

Manipulação eficiente de ROBDDs. Resolução do exercício 6.10 das folhas da cadeira.

T13 - Diagramas de decisão binários.

6 dezembro 2012, 15:00 • Jaime Ramos

Diagramas de decisão binários para representação de funções Booleanas (OBDD). Função determinada por OBDD. Diagramas de decisão binários reduzidos (ROBDD). Existência e unicidade de ROBDD para uma funçã Booleana. Regras de redução. Correcção e completude das regras.

Algumas formas de justiça. Justiça em LTL e em CTL.

Comparação entre a verificação de modelos em LTL e em CTL. vantagens e desvantagens.