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.