Revisao de Modelos CTL~ - IME-USP - Instituto de ...paulotgo/mestrado/dissertacao-slides.pdf · Defesa de Dissertac˘ao de Mestrado~ Paulo de Tarso Guerra Oliveira Orientadora: Profa

Introducao Uma Abordagem para Revisao de Modelos Consideracoes Finais

Revisao de Modelos CTLDefesa de Dissertacao de Mestrado

Paulo de Tarso Guerra OliveiraOrientadora: Profa. Dra. Renata Wassermann

Departamento de Ciencia da ComputacaoInstituto de Matematica e Estatıstica

Universidade de Sao Paulo

16 de dezembro de 2010

Paulo de Tarso Guerra Oliveira Universidade de Sao Paulo

Revisao de Modelos CTL


Agenda

1 IntroducaoVerificacao de SistemasLidando com InconsistenciasUma Abordagem para Atualizacao de Modelos

2 Uma Abordagem para Revisao de ModelosNecessidade de Usar RevisaoRevisao de Modelos CTLAlgoritmo de Revisao

3 Consideracoes FinaisConclusaoTrabalhos Futuros




Introducao




Um Computador Fantastico












Verificacao de Sistemas

Verificacao Formal

Verificacao formal e uma tarefa fundamental no processo dedesenvolvimento de sistemas onde seguranca e um fator crıtico.

Quanto mais cedo um erro e identificado, menos custoso e corrigir-lo.

Verificacao de Modelos CTL

Um eficiente metodo para verificacao formal de sistemas

Caracterısticas: automatico, baseado em modelos, verificacaode propriedades.

Baseada em Logica de Arvore Computacional (CTL)





Verificacao Formal

Verificacao formal e uma tarefa fundamental no processo dedesenvolvimento de sistemas onde seguranca e um fator crıtico.

Quanto mais cedo um erro e identificado, menos custoso e corrigir-lo.

Verificacao de Modelos CTL

Um eficiente metodo para verificacao formal de sistemas

Caracterısticas: automatico, baseado em modelos, verificacaode propriedades.

Baseada em Logica de Arvore Computacional (CTL)





Exemplo de Verificacao de Sistema

EspecificacaoFormal∗

P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u

P6: AG (EF r ∧AF r)

Sistema como umModelo de Kripke

M : p r u

p = sistema desligado; r = sistema executando; u = sistema atualizando;







P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u



M : p r u








P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u



M : p r u





Lidando com Inconsistencias

Mudanca de Crencas

A mudanca de crencas lida com o problema de como um agentedeve adaptar suas crencas de modo a incorporar novas informacoes.

Revisao de Crencas

Lida com mudancas de crencas motivadas por novaspercepcoes sobre mundo.

Postulados AGM (Alchourron, Gardenfors and Makinson, 1985)

Atualizacao de Crencas

Lida com mudancas de crencas motivadas por alteracoes naconfiguracao do mundo.

Postulados KM (Katsuno and Mendelzon, 1991)





Mudanca de Crencas


Revisao de Crencas










Mudanca de Crencas


Revisao de Crencas









Uma Abordagem para Atualizacao de Modelos

Atualizacao de Modelos CTL

Zhang, Y., Ding, Y.: CTL Model Update for System Modifications.Journal of Artificial Intelligence Research 31(1) (2008) 113-155

Uma abordagem para modificacoes de modelos de Kripkeinconsistentes guiadas por princıpios de atualizacao de crencas.

O arcabouco formal de atualizacao de modelos:

Mudancas primitivas em modelos de Kripke

Ordenacao de modelos por proximidade

Criterio de mudancas minimal de modelos

Operador de atualizacao de modelos




Uma Abordagem para Atualizacao de Modelos

Atualizacao de Modelos CTL

Mudancas primitivas

Adicao/Remocao de estado

Adicao/Remocao de transicao

Modificacao do rotulo de um estado

Ordenacao de modelos

M1 6M M2 sse o conjunto de operacoe primitivas que transforma M emM1 esta contido no conjunto que transforma M em M2.

Operador de atualizacao de modelos

Mod(ψ �c φ) =⋃

M∈Mod(ψ) Poss(Update(M, φ))




Uma Abordagem para Revisao de Modelos




Necessidade de Usar Revisao

Problemas ao Usar Atualizacao de Modelos

EspecificacaoFormal

P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u


M : p r u

M ′ : p r u

M ′′ : p r u

Atualizacao de Modelos CTL e uma abordagem adequada quando a propriedade naosatisfeita descreve uma nova funcionalidade, mas nao quando esta propriedade descreveuma funcionalidade que ja desejamos.






EspecificacaoFormal

P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u


M : p r u

M ′ : p r u

M ′′ : p r u







EspecificacaoFormal

P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u


M : p r u

M ′ : p r u

M ′′ : p r u







EspecificacaoFormal

P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u


M : p r u

M ′ : p r u

M ′′ : p r u







EspecificacaoFormal

P1: p

P2: AG (p → AX r)

P3: AG (r → AX (r ∨ u))

P4: AG (u → AX (r ∨ u))

P5: EFAG u


M : p r u

M ′ : p r u

M ′′ : p r u







Guerra, P. T., Wassermann, R.: Revision of CTL Models. Advances inArtificial Intelligence - IBERAMIA 2010, LNCS, vol. 6433, p. 152-162.

Uma abordagem para modificar modelos de Kripke baseada emprincıpios de revisao de crencas.

O arcabouco formal de revisao de modelos:

Ordenacao por proximidade entre modelos e conj. de modelos

Criterio de revisao minimal de modelos

Operador de revisao de modelos






Definicao de proximidade de ZD08

6M :

Mod(φ)

−→

M ∈ Mod(ψ)

=⇒

Atualizacao

Nova definicao de proximidade

6Mod(ψ):

Mod(φ)

−→

Mod(ψ)

=⇒

Revisao






Definicao de proximidade de ZD08

6M :

Mod(φ)

−→

M ∈ Mod(ψ)

=⇒

Atualizacao

Nova definicao de proximidade

6Mod(ψ):

Mod(φ)

−→

Mod(ψ)

=⇒

Revisao






Operador de Revisao de Modelos

Mod(ψ ◦c φ) = MinMod(ψ)(Mod(φ))

onde MinB(A) denota o conj. de modelos de A minimais com relacao a 6B.

Teorema 8

O operador ◦c satisfaz os postulados de revisao (R1)-(R6).






Operador de Revisao de Modelos

Mod(ψ ◦c φ) = MinMod(ψ)(Mod(φ))

onde MinB(A) denota o conj. de modelos de A minimais com relacao a 6B.

Teorema 8

O operador ◦c satisfaz os postulados de revisao (R1)-(R6).






Modelos que satisfazem AG (EF r ∧ AF r)

M ′ : p r u M ′′ : p r u

Modelos que satisfazem a especificacao formal

M : p r u

M2 : p r u

M3 : p r u







M ′ : p r u M ′′ : p r u


M : p r u M2 : p r u

M3 : p r u







M ′ : p r u M ′′ : p r u



M3 : p r u







M ′ : p r u

M ′′ : p r u



M3 : p r u




Algoritmo de Revisao

Algoritmo Conceitual

ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






ψ

¬φ φ






Gerar modelos admissıveisde cada modelo de entrada.

Ordenar os modelos ge-rados pela proximidadeao conjunto de entrada.

Descartar mode-los nao-minimais.

Modelos de ψ φ

Modelos revisados

Mudancas minimaismodelo-a-modelo.





Algoritmo Proposto

Caracterısticas:

Iteracao sobre decomposicao de formulas

Mudancas minımas a cada recursao

Geracao de multiplas possibilidades de correcao

Restrito a um conjunto finito de entrada





Problemas no Desenvolvimento do Algoritmo

Problemas praticos:

Problemas com as funcoes de [ZD08]

Redefinicao de RevisaoEX ,RevisaoAF e RevisaoEU

Formulacao de Revisao¬EX ,Revisao¬AF e Revisao¬EU

Selecao de um subconj. de Mod(ψ)

Funcoes devem gerar todas asmodificacoes possıveis






Problemas praticos:











Problemas praticos:









Consideracoes Finais




Conclusao

Conclusao

Problemas da atualizacao de modelos em contextos estaticos

Formalizacao do conceito de revisao de modelos

Arcabouco formal para revisao de modelos CTL

Discussoes sobre o algoritmo de revisao de modelos

Nao e promissor desenvolver uma abordagem para revisao demodelos espelhado no metodo de Zhang e Ding




Trabalhos Futuros

Trabalhos Futuros

Mais analise de propriedades semanticas

Estudo das propriedades computacionais

Desenvolvimento de uma algoritmo pratico

Estender o conceito para outras logicas




Trabalhos Futuros

Obrigado!

Durante o desenvolvimento deste trabalho o autor recebeu auxılio financeiro do CNPQ.



Documents

Revisao de Modelos CTL~ - IME-USP - Instituto de ...paulotgo/mestrado/dissertacao-slides.pdf · Defesa de Dissertac˘ao de Mestrado~ Paulo de Tarso Guerra Oliveira Orientadora: Profa