Verificação 20/03/2012

   # # # # # # # # # # # # #
  # Verificação Automatica  #
  # Prof. Sérgio Campos     #
  # notasdogarcia.blog.com  #
   # # # # # # # # # # # # #

  Vamos falar de modelo de computação

  Estamos falando de uma estrutura de Kripke que é uma arvore infinita de computação, que na prática é expressa de forma finita.

  É composta por uma tripla:
  S = Estados ex: (1,2,3)
  R = Transições (1,2) (1,3) (2,2) (3,1) etc..
  L = Quais variáveis são verdades em quais pontos ex: (1 -> a,b) (2 -> c) (3 -> a,c)

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Primeira lógica que falaremos:

  CTL* (CTL asterisco é o nome)

  Temos 2 t ipos de operadores:

  De caminho:
    - A -: para todos os caminhos
    - E -: para algum caminho

  De lógica temporal:
    - G, F, X, U

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  Formulas de Estado:

    Se s é uma formula de estado então a notação M.s |= f implica que f é verdade no estado s que pertence ao grafo M.

    s |= E(g) diz que existe um caminho em s tal que g é satisfeito.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  Formulas de Caminho:

    Um caminho c satisfaz uma propriedade do tipo M.s |= c se a propriedade definida por c é mantida nos estados sucessores de s.

 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

  // Todos os caminhos são infinitos
  // Toda propriedade de estado é uma de caminho, basta pensar que se o estado atual satisfizer então o caminho e verdade nesse estado.


  Abreviações:
  A(f) == !E(!f)
  F(f) == true U f
  G(f) == !F !f

  São 3 logicas: CTL LTL e CTL estrela.
  Computation Tree Logic
  Linear Time Logic

  não se tem em ctl a formula A(FG p)
  nao se tem em LTL AG(EF p)

  nao se tem nem em CTL Nem em LTL A(FG p) || AG(EF p) (mas se tem em CTL* que é a junção dos 2)
  // por motivos obvios.

  vamos tentar lidar com uma e outra ao invez de usar o CTL* que engloba as duas o tempo todo.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  8 operadores CTL:
    AX and EX
    AG and EG
    AF and EF
    AU and EU

  Cada um dos operadores acima voce consegue reduri a EX EG e EU
  Isso é bom na hora de construir o model checker pq voce pode construir só 3 funções =].
  O professor mostrou as equivalencias, mas não anotei.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  Como provar EF p, ou seja Existe um caminho onde Fatalmente p será verdade.
  Para provar voce pode partir do caso base, onde a afirmaçào é verdade se p é verdade no estado inicial.

  Depois voce vai na ideia, que o caminho é verdade no estado s se existir um sucessor de s onde o caminho seja verdade.

  A cada interação então voce pode mostrar para cada estado onde o caminho é verdade que o caminho também é verdade para seus antecessores.
  Quando uma interação não gerar nenhuma alteração no grafo, significa que todos os estados foram encontrados.

// fim da aula.