Revisão de Modelos CTL
Paulo de Tarso Guerra Oliveira
Renata Wassermann
Departamento de Ciência da Computação
Instituto de Matemática e Estatı́stica
Universidade de São Paulo
Resumo Verificação de modelos é uma das mais eficientes técnicas de
verificação automática de sistemas. No entanto, as ferramentas de verificação usualmente não fornecem informações sobre como reparar inconsistências. Em nossa dissertação, mostramos que abordagens desenvolvidas para a atualização de modelos inconsistentes da lógica de árvore
computacional (CTL) não são capazes de lidar com todos os possı́veis
tipos de alterações em modelos. Introduzimos então o conceito de revisão
de modelos CTL: uma abordagem baseada em revisão de crenças para o
reparo de modelos inconsistentes em um contexto estático. Relacionamos
nossa proposta com trabalhos clássicos em revisão de crenças, definimos
um operador de revisão de modelos e mostramos que este obedece postulados de racionalidade clássicos de revisão de crenças. Elaboramos um
algoritmo de revisão baseado no algoritmo utilizado pela abordagem de
atualização de modelos. Discutimos sobre problemas e limites deste algoritmo e mostramos que essa estratégia de adaptação não é uma solução
apropriada.
Palavras-chave: Revisão de crenças, lógica de árvore computacional,
verificação de modelos
Sobre o Trabalho
Nı́vel: Dissertação de Mestrado. Data de conclusão: 16 de dezembro de 2010.
Banca examinadora: Profa. Dra. Renata Wassermann (IME - USP), Profa.
Dra. Leliane Nunes de Barros (IME - USP), Prof. Dr. Paulo Eduardo Santos
(FEI). Versão on-line da dissertação: http://www.ime.usp.br/~paulotgo/
mestrado/dissertacao.pdf. Publicações derivadas: resumo expandido “Belief Revision on Computation Tree Logic [8]” nos proceedings da 20th International Joint Conference on Artificial Intelligence (IJCAI’11 Doctoral Consortium);
artigo completo “Revision of CTL Models [7]” nos proceedings da 12th IberoAmerican Conference on Artificial Intelligence (IBERAMIA’10).
1
Introdução
Verificar formalmente um sistema é uma maneira de assegurar que erros de projeto não se propaguem para a implementação do sistema. No entanto, as atuais
ferramentas de verificação não possuem mecanismos que auxiliem o projetista
no reparo de modelos de sistema incorretos.
Proposta por Clarke e Emerson, a verificação de modelos [4,10] permite que
o projetista verifique quando um modelo de sistema satisfaz (ou não) uma dada
especificação formal. Uma especificação formal nada mais é que o conjunto de
propriedades que definem o comportamento do sistema. Quando alguma dessas
propriedades não é satisfeita, temos o que chamamos de inconsistência de especificação. Nas últimas décadas, muitos trabalhos aprimoraram a verificação de
modelos, resultando em eficientes algoritmos de verificação.
Contudo, a maioria das ferramentas de verificação, quando encontram uma
inconsistência de especificação, apenas informam o caminho que a ocasiona (caminho contraexemplo). Apesar de útil, essa informação pode não ser suficiente
para indicar como o modelo deve ser reparado. Quanto mais complexo o sistema,
mais complexa é sua modelagem e assim, mais difı́cil é corrigir seus erros. Em
geral, ferramentas de verificação não possuem mecanismos capazes de auxiliar
na tarefa de correção, o que não as credencia como ferramentas completas para
o reparo de sistemas.
Sendo possı́vel implementar a verificação de modelos por meio de algoritmos
rápidos e eficazes, o problema se voltou a como construir ferramentas capazes
de corrigir automaticamente modelos inconsistentes de sistemas.
1.1
Motivação
Buccafurri et al [2] foi o primeiro trabalho a desenvolver um arcabouço formal
integrando verificação de modelos e revisão abdutiva de teorias para realizar o
diagnóstico e reparo de erros em programas concorrentes.
Contudo, apesar de ser bem sucedida para seus propósitos, o conceito de
modificação adotado é um tanto restrito. Zhang e Ding [16] propõem um arcabouço para atualização de modelos que supre as deficiências apresentadas pelo
método de Buccafurri et al.. Seu arcabouço está fundamentado em princı́pios de
mudanças de crenças.
A mudança de crenças possui duas principais vertentes: revisão de crenças
[1] e atualização de crenças [12]. A revisão de crenças trata de como um agente
deve incorporar informações sobre um mundo estático, onde a nova crença refina
ou corrige o conhecimento do agente sobre o mundo. Já a atualização de crenças
lida com informações provenientes de mudanças no mundo, mudanças essas que
alteram a maneira como o agente deve interpretá-lo.
Zhang e Ding [16] propuseram um arcabouço para o que chamaram de atualização de modelos CTL, uma integração entre os conceitos de verificação de
modelos e de atualização de crenças. Eles especificaram um procedimento para
a atualização mı́nima de modelos e analisaram suas propriedades semânticas e
computacionais.
Apesar da similaridade entre atualização de crenças e revisão de crenças, o
uso da abordagem incorreta pode acarretar em significativa perda de informação.
Em [7] argumentamos que uma abordagem baseada em atualização de crenças
não é apropriada para todos os casos.
Essa é a nossa principal motivação para formulação de uma nova abordagem
baseada em revisão de crenças para mudanças em modelos quando o reparo de
especificações ocorrer em um contexto estático.
1.2
Justificativa
A revisão de especificações não pode ser realizada pela simples aplicação da
revisão de crenças. Isso porque nem todos os resultados conhecidos de revisão de
crenças podem ser aplicados nessa abordagem. A verificação de modelos baseiase em lógicas temporais, contudo a maioria dos resultados obtidos assumem
propriedades que essas lógicas não possuem.
Souza e Wassermann [14] abordam o uso prático de revisão de crenças para
o reparo de modelos inconsistentes. Os autores criaram uma ferramenta capaz
de gerar sugestões de reparo para modelos descrito segundo a linguagem SMV.
Acreditamos no entanto que a técnica poderia explorar melhor os conceitos de
revisão, sendo possı́vel desenvolver uma abordagem que possua fundamentos
sólidos na teoria clássica de revisão de crenças.
Direcionamos nossa dissertação à formalização do conceito de revisão de modelos CTL: uma abordagem baseada em revisão de crenças para o reparo de
modelos inconsistentes em um contexto estático. Relacionamos nossa proposta
a trabalhos clássicos em revisão de crenças e discutimos questões relativas a sua
implementação.
1.3
Contribuições
As principais contribuições do nosso trabalho são:
1. Esclarecemos a diferença entre revisão de modelos e atualização de modelos. Mostramos que existem casos onde a atualização gera resultados menos
significativos do que o esperado, sendo a revisão de modelos mais adequada.
2. Propomos um arcabouço formal para revisão de modelos CTL. Utilizamos as
operações primitivas de Zhang e Ding [16] para definir o critério de mudança
minimal. Estudamos a relação entre nossa proposta de revisão de modelos e
a abordagem tradicional de revisão de crenças, em especial mostramos que
nosso operador obedece os postulados AGM [1] para revisão.
3. Desenvolvemos um algoritmo formal para revisão de modelos CTL. Dados
um conjunto de modelos que satisfazem uma especificação e uma propriedade
expressa por uma fórmula CTL, nosso algoritmo é capaz de gerar modelos
que satisfazem esta propriedade e que se diferenciam minimamente daqueles fornecidos como entrada. Estes modelos gerados podem ser vistos como
possı́veis correções para a especificação original.
2
2.1
Fundamentação Teórica
Lógica de Árvore Computacional
Lógicas temporais são um tipo de lógica modal onde podemos representar e
raciocinar sobre o tempo. Lógica de árvore computacional (Computation Tree
Logic, ou simplesmente CTL)[4,10] é uma lógica temporal que modela o futuro
como ramificações de uma árvore e, devido a isso, pode quantificar sobre os
diversos caminhos de execução que um sistema pode tomar. Nas definições 1 e
3, mostramos brevemente a sintaxe e semântica da CTL (ver [10] para maiores
detalhes).
Definição 1 (Sintaxe). Uma fórmula CTL tem a seguinte sintaxe:
ϕ ::= > | p | (¬ϕ) | (ϕ ∧ ϕ) | EXϕ | EGϕ | E[ϕU ϕ]
onde p é uma fórmula atômica, ¬, ∧ os conectivos lógicos clássicos e os demais
elementos os operadores temporais.
Usamos ⊥ para denotar ¬>, e outros operadores temporais podem ser derivados de EX, EG e EU : AXφ = ¬EX¬φ; AGφ = ¬EF¬φ; AFφ = ¬EG¬φ; EFφ
= E[>Uφ]; A[φUβ] = ¬E[¬βU¬φ ∧ ¬β] ∧ ¬EG¬β.
Cada operador temporal consiste de um quantificador de caminho (E, “existe
um caminho”, or A, “para todos os caminhos”) seguido por um quantificador de
estado (X, “próximo estado”, U, “até que”, G, “todos os estados” or F, “algum
estado futuro”).
Definição 2. Seja P um conjunto finito de proposições, um modelo de Kripke
é uma tripla M = (S, R, L), onde
1. S é um conjunto de estados;
2. R ⊆ S × S, onde ∀s ∈ S, ∃s0 ∈ S tal que (s, s0 ) ∈ R;
3. L : S → 2P é uma função de rotulação, tal que ∀s ∈ S, L(s) determina todas
as proposições verdadeiras em s.
Deste ponto em diante, sempre que nos referirmos à um modelo CTL estamos
na verdade nos referindo a um modelo de Kripke conforme a Definição 2.
Definição 3 (Semântica). Seja M = (S, R, L) um modelo CTL, s ∈ S um
estado de M e φ uma fórmula CTL. Definimos (M, s) φ indutivamente como
(M, s) >.
(M, s) p sse p ∈ L(s).
(M, s) ¬φ sse (M, s) 6 φ.
(M, s) φ1 ∧ φ2 sse (M, s) φ1 e (M, s) φ2 .
(M, s) EXφ sse ∃s0 ∈ S tal que (s, s0 ) ∈ R e (M, s0 ) φ.
(M, s) EGφ sse existe um caminho π = [s0 , s1 , . . . ] em M tal que s0 = s
e (M, si ) φ para todo i ≥ 0.
7. (M, s) E[φ1 U φ2 ] sse existe um caminho π = [s0 , s1 , . . . ] em M tal que
s0 = s, ∃i ≥ 0, (M, si ) φ2 e ∀j < i, (M, sj ) φ1 .
1.
2.
3.
4.
5.
6.
Dado um modelo CTL M = (S, R, L) e seu conjunto de estados iniciais
Init(S) ⊆ S, dizemos que M φ se e somente se (M, s) φ para algum
s ∈ Init(S).
2.2
Verificação de Modelos CTL
Métodos de verificação formal checam quando um modelo de sistema, descrito
em uma linguagem formal, satisfaz um dado conjunto de propriedades desejadas. Verificação de modelos [4,10] é provavelmente o método de verificação mais
comumente utilizado. Segundo [4], verificação de modelos consiste no processo
de computar a resposta para o problema de checar quando (M, s) φ vale, onde
φ é uma formula temporal, M é um modelo do sistema em consideração, s um
estado desse modelo, e a relação de satisfação.
Neste trabalho, nós assumimos apenas um tipo de verificação de modelos,
a verificação de modelos CTL. Nós assumimos que os sistemas são descritos
por estruturas de Kripke e que as propriedades desejadas são representadas por
formulas CTL.
2.3
Revisão de Crenças
Revisão de crenças trata do problema de adaptar a crença de um agente a fim
de incorporar um nova informação, possivelmente inconsistente como o que o
agente costumava acreditar. Em [1], Alchourrón, Gärdenfors e Makinson propuseram um conjunto de postulados os quais métodos de revisão de crenças
devem satisfazer, bem como construções de funções de revisão que obedecem
estes postulados. Este trabalho se tornou conhecido como o Paradigma AGM.
Os postulados AGM guiam as operações de revisão através de um princı́pio de
mudança mı́nima, isto é, nada deve ser adicionado (ou removido) de um conjunto
de crenças exceto se extremamente necessário para o sucesso da revisão. SejaK
um conjunto de crenças e α uma única crença, denotamos por K ∗ α o resultado
de revisar K por α.
A operação K ∗ α não possui uma única definição, mas é sempre restringida pelos postulados de racionalidade. Aqui, utilizamos a notação adotada em
[11], onde os autores sugerem a reformulação dos postulados AGM quando um
conjunto de crenças é representado por uma única sentença ψ. O resultado da
revisão de ψ por φ é denotado por ψ ◦ φ:
(R1) ψ ◦ φ φ.
(R2) Se ψ ∧ φ é satisfazı́vel, então ψ ◦ φ ≡ ψ ∧ φ
(R3) Se φ é satisfazı́vel, então ψ ◦ φ é satisfazı́vel.
(R4) Se ψ1 ≡ ψ2 e φ1 ≡ φ2 , então ψ1 ◦ φ1 ≡ ψ2 ◦ φ2 .
(R5) (ψ ◦ φ) ∧ µ ψ ◦ (φ ∧ µ)
(R6) Se (ψ ◦ φ) ∧ µ é satisfazı́vel, então ψ ◦ (φ ∧ µ) (ψ ◦ φ) ∧ µ
2.4
Atualização de Crenças
O propósito da atualização de crenças, assim como a revisão de crenças, é preservar a consistência de um conjunto de crenças quando uma nova informação
é adicionada. Enquanto a revisão lida com mundos estáticos, a atualização de
crenças atua sobre mundos dinâmicos, onde a nova informação descreve mudanças que ocorreram no mundo. Esta é a distinção fundamental entre elas: a
natureza da mudança de crença.
Em revisão de crenças, a nova informação indica um refinamento do conjunto
de crenças, ou mesmo que as crenças atuais não são capazes de descrever o mundo
corretamente. Mas em atualização de crenças, a nova informação indica uma
mudança e o resultado da atualização não se refere a como o mundo costumava
ser, apenas como ele estará após a mudança. O Exemplo 1 ilustra bem a distinção
entre revisão e atualização.
Exemplo 1. Imagine que um quarto existem três objetos: um livro, uma revista
e uma mesa. A proposição b significa “o livro está sobre a mesa” enquanto
que m significa “a revista está sobre a mesa”. Suponha que acreditamos que
ψ ↔ (b ∧ ¬m) ∨ (¬b ∧ m), isto é, ou o livro ou a revista está sobre a mesa,
mas não ambos. Assim, ψ possui apenas dois mundos (modelos) possı́veis: I, b
é verdade e m falso; ou J, b é falso e m é verdade.
Suponha agora que enviamos um robô para pôr o livro sobre a mesa. Desejamos então incorporar a nossas crenças a nova informação φ ↔ b. Está nova
crença também possui dois únicos modelos: I e um novo L, onde ambos, livro e
revista, estão sobre a mesa. Devemos selecionar dentre os modelos de φ os mais
próximos aos modelos de ψ. Assumiremos como relação de distância o número
de proposições com diferentes valores verdade. O modelo I está, claro, a uma
distância 0 dele mesmo e a uma distância 2 de J (ambas proposições diferentes).
Por outro lado, L está a uma distância 1 de I e J (uma posição diferente).
O operador de revisão irá selecionar apenas o modelo I porque este é o modelo
mais próximo (distância 0) do conjunto original. Mas intuitivamente isso não nos
parece correto. Após o robô executar sua ação, tudo que sabemos é que o livro
estará sobre a mesa, mas continuamos sem saber a posição da revista.
Katsuno e Mendelzon [12] propuseram um conjunto de postulados para caracterizar operações racionais de atualização. Seja ψ uma fórmula que representa
uma base de crenças finita, φ a nova crença e ψ ψ o resultado da atualização
de ψ por φ, os oito postulados definidos por Katsuno e Mendelzon são:
(U1)
(U2)
(U3)
(U4)
(U5)
(U6)
(U7)
(U8)
ψ φ φ.
Se ψ φ, então ψ φ ≡ ψ.
Se ambos ψ e φ são satisfazı́veis, então ψ φ é também satisfazı́vel.
Se ψ1 ≡ ψ2 e φ1 ≡ φ2 , então ψ1 φ1 ≡ ψ2 φ2 .
(ψ φ) ∧ µ ψ (φ ∧ µ)
Se ψ φ1 φ2 e ψ φ2 φ1 , então ψ φ1 ≡ ψ φ2
Se ψ é completo, então (ψ φ1 ) ∧ (ψ φ2 ) ψ (φ1 ∨ φ2 )
Se (ψ1 ∨ ψ2 ) φ ≡ (ψ1 φ) ∨ (ψ2 φ)
Herzig [9] mostra que, mais que distintos, revisão e atualização são mutualmente incompatı́veis, já que não pode existir um operador capaz de satisfazer os
dois conjunto de postulados simultaneamente.
2.5
Atualização de Modelos CTL
No contexto das mudanças em especificações formais, modelos são descritos por
modelos de Kripke e propriedades por fórmulas CTL. Zhang e Ding [16] definem
cinco operações básicas onde todas as mudanças possı́veis sobre modelo M =
(S, R, L) podem ser alcançadas:
PU1:
PU2:
PU3:
PU4:
PU5:
Adicionar um par ao conjunto R
Remover um par do conjunto R
Alterar a função de rotulação de um estado em S
Adicionar um estado à S
Remover um estado isolado de S
Dados dois modelos CTL, M = (S, R, L) e M 0 = (S 0 , R0 , L0 ), para cada
P U i (i = 1, . . . , 5), denotamos por Dif fP U i (M, M 0 ) a diferença entre M e M 0 ,
onde M 0 é um modelo atualizado de M , tal que
1.
2.
3.
4.
5.
Dif fP U 1 (M, M 0 ) = R0 − R (relações adicionadas);
Dif fP U 2 (M, M 0 ) = R − R0 (relações removidas);
Dif fP U 3 (M, M 0 ) = {s | s ∈ S ∩ S 0 and L(s) 6= L0 (s)} (mudanças de rótulo);
Dif fP U 4 (M, M 0 ) = S 0 − S (estados adicionados);
Dif fP U 5 (M, M 0 ) = S − S 0 . (estados removidos).
Baseados nessas métricas, Zhang e Ding definem a ordem ≤M : uma medida
da diferença entre dois modelos CTL com respeito a um terceiro modelo M .
Definição 4. Sejam M = (S, R, L), M1 = (S1 , R1 , L1 ) e M2 = (S2 , R2 , L2 )
três modelos CTL. Dizemos que M1 é pelo menos tão próximo de M quanto
M2 , denotado por M1 ≤M M2 , se e somente se para cada conjunto de operações
PU1-PU5 que transformam M em M2 , existe um conjunto de operações PU1PU5 que transformam M em M1 tal que:
1. para cada i (i = 1, . . . , 5), Dif fP U i (M, M1 ) ⊆ Dif fP U i (M, M2 ), e
2. se Dif fP U 3 (M, M1 ) = Dif fP U 3 (M, M2 ), então ∀s ∈ Dif fP U 3 (M, M1 ),
dif f (L(s), L1 (s)) ⊆ dif f (L(s), L2 (s)), onde dif f (A, B) = (A−B)∪(B −A)
para qualquer dois conjuntos A e B.
Denotamos por M1 <M M2 se M1 ≤M M2 e M2 6≤M M1 .
Baseado nessa relação de ordem, os autores definem formalmente o conceito
de atualização admissı́vel:
Definição 5. Dado um modelo M = (S, R, L), M = (M, s0 ), onde s0 ∈ S,
e uma fórmula CTL φ, um modelo U pdate(M, φ) é dito uma atualização admissı́vel de M se as seguintes condições valem:
1. U pdate(M, φ) = (M 0 , s00 ), (M 0 , s00 ) φ, onde M 0 = (S 0 , R0 , L0 ) e s00 ∈ S 0 .
2. não existe outro modelo M 00 = (S 00 , R00 , L00 ) e s000 ∈ S 00 tal que (M 00 , s000 ) φ
e M 00 <M M 0 .
P oss(U pdate(M, φ)) denota o conjunto de todos as atualizações admissı́veis de
M para satisfazer φ.
A principal contribuição do trabalho de Zhang e Ding é talvez a análise
semântica da atualização de modelos CTL. Eles relacionam sua abordagem a
abordagens clássicas de atualização de crenças, identificando pontos em comum
entre elas. Para isso, os autores definem um operador c baseado na abordagem
de modelos possı́veis de Winslett [15]. A definição formal de c é dada por:
Definição 6. Seja M = (S, R, L) um modelo CTL, Init(S) ⊆ S o conjunto de
estados iniciais de M e φ uma fórmula CTL. M é chamado um modelo de φ
se e somente se (M, s) φ para algum s ∈ Init(S). Denotamos por M od(φ) o
conjunto de todos os modelos de φ. O operador de atualização de modelos c é
definido como:
[
M od(ψ c φ) =
P oss(U pdate((M, s), φ))
(M,s)∈M od(ψ)
Zhang and Ding ([16], Teorema 1) demonstram que o operador c satisfaz
todos os postulados de Katsuno e Mendelzon para atualização. Dessa forma,
eles evidenciam que estes postulados podem caracterizar um escopo mais amplo
de operadores de atualização do que apenas a tradicional aplicação em lógica
proposicional. Neste sentido, Zhang e Ding mostram que os postulados KM são
essenciais para qualquer abordagem baseada em atualização de modelos.
3
Nossa Abordagem: Revisão de Modelo CTL
A necessidade da revisão de modelos CTL é motivada pela diferença fundamental
entre revisão de crenças e atualização de crenças: o tipo de problema em que
cada um deve ser aplicada. Como vimos nas seções 2.3 e 2.4, atualização de
crenças é usada para modificar um conjunto de crenças de modo a acomodar
uma nova informação sobre um mundo dinâmico, enquanto a revisão de crenças
é usada quando a nova informação diz respeito a um mundo que não mudou.
Para ilustrar uma situação onde revisão de crenças é mais adequada, voltemos
ao Exemplo 1. Vimos que um operador de atualização geraria a nova base de
crença ψ 0 ↔ b, enquanto que um operador de revisão geraria uma base ψ 00 ↔
(b ∧ ¬m). Intuitivamente, a atualização resulta em um comportamento mais
racional, já que a situação não nos fornece qualquer informação sobre a posição
da revista.
Suponha porém que, em vez de enviar o robô para pôr o livro sobre a mesa,
desejamos apenas saber a posição do livro, sem alterá-la. Suponha então que
quando o robô sai da sala ele nos informa que o livro está sobre a mesa. A nova
crença é a mesma, φ ↔ b e, consequentemente, os resultados da revisão e da
atualização serão idênticos ao do caso anterior. No entanto, nesta nova situação
o resultado da revisão parece mais apropriado.
De acordo com a informação φ ↔ b, duas configurações do quarto são
possı́veis: (1) o livro está sobre a mesa e a revista no chão (b ∧ ¬m) ou (2)
ambos, livro e revista, estão sobre a mesa (b ∧ m). Na situação onde enviamos
um robô para observar a sala, nós costumávamos acreditar que o livro e a revista
não estavam no mesmo lugar. Sabemos que nada no quarto mudou, então não
há razão para termos dúvidas sobre a localização da revista. Podemos ver que
nesta situação a revisão produziu um resultado mais informativo.
Observe que, em ambos casos, a base de crenças ψ e a nova informação φ
são as mesmas, o que muda é como o indivı́duo interage com o mundo, e, claro,
o modo como devemos interpretar isso. Acreditamos que o mesmo problema de
distinção entre mundos estáticos e dinâmicos acontece quando lidamos com o
reparo de especificações de sistemas.
Existem dois principais motivos para modificar uma especificação de sistema:
(1) quando ela falha em satisfazer algum requisito e (2) quando ela precisa ser
adaptada a um novo requisito. Quando modificamos uma especificação motivado
por (1), nós acreditamos que repará-la por meio de uma abordagem baseada em
revisão de crenças pode gerar um resultado mais informativo que aquele gerado
pela atualização de modelos CTL, de um modo similar ao que ocorre entre
revisão e atualização de crenças.
Uma abordagem baseada em revisão de crenças para tratar especificações
inconsistentes foi apresentada em [13,14]. Nesta abordagem, os autores enriqueceram o verificador NuSMV [3] como princı́pios de revisão de crença, o que
resultou na ferramenta BrNuSMV1 : uma ferramenta capaz de gerar sugestões de
modificação para uma dada especificação de sistema tal que alguma propriedade
CTL se torne válida.
Talvez por ser um passo inicial na integração da verificação de modelos e
princı́pios de revisão de crenças, existem no BrNuSMV algumas lacunas: não
é possı́vel tratar todos os tipos de fórmulas CTL; o processo de revisão é feito
estado à estado, com limitações nos conjuntos de crenças; não há uma análise
formal do processo de revisão de modelos. No nosso trabalho, nos propomos a
preencher algumas dessas lacunas, realizando uma análise formal do processo de
revisão de modelos CTL genéricos e estudar sua relação com abordagens clássicas
de revisão de crenças.
Nosso operador de revisão ◦c sobre modelos CTL é definido por:
Definição 7. Dadas duas fórmulas CTL ψ e φ, denotamos por ψ ◦c φ uma
fórmula CTL resultado da atualização de ψ por φ, tal que
M od(ψ ◦c φ) = M inM od(ψ) (M od(φ))
onde M inB (A) denota o conjunto de todos os modelos minimais de A com respeito a todas as ordens ≤M tal que M é um modelo de B.
Teorema 1. O operador ◦c satisfaz os postulados de revisão (R1)-(R6).2
No algoritmo 1, nós apresentamos um esboço do algoritmo de revisão de
modelos CTL. Dado uma base de crenças ψ e uma nova crença φ, ambas representadas por fórmulas CTL, o algoritmo de revisão computa um conjunto S de
modelos CTL tais que todo modelo M ∈ S, M ∈ M od(ψ ◦c φ).
1
2
Acrônimo para Belief Revision NuSMV.
A prova foi omitida por limitações de espaço e pode ser vista em [6].
Algoritmo 1 CTLModelRevision(ψ, φ)
Entrada: Duas fórmulas CTL ψ e φ, representando a base de crenças e a nova crença,
respectivamente.
Saı́da: Um conjunto de modelos CTL S tal que S ⊆ M od(ψ ◦c φ).
1: S ← ∅;
2: para todos modelos M = (S, R, L) tal que M ∈ M od(ψ) faça
3:
se M φ vale então
4:
S ← S ∪ {M };
5:
senão
6:
repita
7:
S ← S ∪ CT LU pdate((M, s), φ), onde s ∈ Init(S);
8:
até não haver mudança em S.
9: para todos modelos M = (S, R, L) tal que M ∈ M od(ψ) faça
10:
S ← S − {M 0 |{M 0 , M 00 } ⊆ S and M 00 <M M 0 };
11: devolva S.
Primeiro, nós iniciamos S como vazio. Nas linhas 2-8, iteramos sobre os
modelos de ψ para achar aqueles que satisfazem φ. Se um modelo M de ψ
satisfaz φ, então M é adicionado à S, caso contrário, nas linhas 6-8, procuramos
por todos os modelos possı́veis que satisfazem φ e que são próximos à M . Para
isso, fazemos sucessivas chamadas à CT LU pdate((M, s), φ), função descrita em
[16]. Nas linhas 9-10, nós removemos de S todos os modelos que não são minimais
em relação aos modelos de ψ. Após esse passo, todos os modelos em S satisfazem
φ e são mı́nimos com respeito à ≤M . Finalmente retornamos S.
Zhang and Ding [16], Teorema 8, afirma que CT LU pdate((M, s), φ) sempre
gera um modelo M 0 que satisfaz φ e é minimal segundo a Definição 4. No entanto,
não há garantias que CT LU pdate((M, s), φ) é capaz de gerar todos os modelos
minimais possı́veis, portanto não podemos assegurar que nosso algoritmo pode
obter S = M od(ψ ◦c φ) como resultado.
Zhang and Ding [16] não definem um algoritmo de atualização de modelos
CTL. A fim de comparar as abordagens de atualização e revisão de modelos
CTL, nós especificamos um método de atualização de modelos (Algoritmo 2)
baseados no operador c definido por eles.
A diferença entre estas duas abordagens é ilustrada no Exemplo 2.
Exemplo 2. Seja p e q dois átomos proposicionais e ψ ↔ EXAGp nossa base
de crenças. Suponha que nós precisamos modificar ψ de modo a aceitar φ ↔
E[pU q]. Suponha também que φ não descreve uma mudança no mundo, apenas
uma nova informação. Sabemos que M1 = ({s0 , s1 }, {(s0 , s1 ), (s1 , s1 )}, {L(s0 ) =
{p}, L(s1 ) = {p}} e M2 = ({s0 , s1 }, {(s0 , s1 ), (s1 , s1 )}, {L(s0 ) = {q}, L(s1 ) =
{p}} pertencem à M od(ψ). Quando nós submetemos ψ e φ ao método de atualização de modelos, nós obtemos um modelo M10 = ({s0 , s1 , s2 }, {(s0 , s1 ), (s1 , s1 ),
(s1 , s2 )}, {L(s0 ) = {p}, L(s1 ) = {p}, L(s2 ) = {q}}, o qual não pertence ao resultado do algoritmo de revisão de modelos CTL. Apesar de M10 ser minimal em
relação à M1 , M10 não é minimal em relação a todos os modelos de ψ (já que M2
satisfaz φ e M2 <M2 M10 ), portanto M10 não pertence a M od(ψ ◦c φ) e é removido
no último laço do algoritmo de revisão.
Algoritmo 2 CTLModelUpdate(ψ, φ)
Entrada: Duas fórmulas CTL ψ e φ, representando a base de crenças e a nova crença,
respectivamente.
Saı́da: Um conjunto de modelos CTL S tal que S ⊆ M od(ψ c φ).
S ← ∅;
para todos modelos M = (S, R, L) tal que M ∈ M od(ψ) faça
se M φ vale então
S ← S ∪ {M };
senão
repita
S ← S ∪ CT LU pdate((M, s), φ), onde s ∈ Init(S);
até não haver mudança em S.
devolva S.
4
Conclusões
Verificadores de modelos são ferramentas importantes no desenvolvimento de
sistemas, mas que não possuem mecanismos que auxiliam na correção de inconsistências. Diversos autores exploraram a integração entre técnicas de Inteligência Artificial e verificação de modelos [2,5,14,16]. Neste trabalho apresentamos um estudo formal de revisão de crenças como técnica para o reparo de
modelos inconsistentes. Mostramos que revisão de crença pode ser uma poderosa
ferramenta de auxilio à modelagem formal de sistemas computacionais.
Argumentamos que a abordagem de Zhang e Ding [16] não é adequada para
todas as situações de reparo de sistemas. Mostramos que, nos casos em que
mudanças significam correções e não adaptações, nossa abordagem baseada em
revisão de crenças é mais apropriada que uma baseada em atualização. Mostramos que, nestas situações, nosso cálculo de novos modelos conserva um maior
grau de coerência com a especificação original do sistema.
A existência de uma revisão AGM é assegurada apenas para lógicas compactas e monotônicas, porém CTL não satisfaz esta primeira propriedade. Não
podemos aplicar diretamente a teoria existente para a revisão de modelos CTL.
Apresentamos uma primeira abordagem de integração de revisão de crenças
e verificação de modelos, denominada BrNuSMV [13,14]. Mostramos que apesar
de uma aplicação prática, essa abordagem possui algumas limitações. Buscamos
então preencher algumas das lacunas apresentada por essa.
Propusemos um arcabouço formal para revisão de modelos CTL. Primeiro,
definimos o critério de ordenação entre dois modelos CTL (baseado na distância
deste a um dado conjuntos de modelos). Formalizamos então nosso operador de
revisão, onde, baseado na ordenação definida, estabelecemos o critério de minimalidade para a escolha de modelos consistentes. Mostramos que nosso operador
de revisão obedece os postulados de revisão AGM, conforme reformulação de [11].
Desenvolvemos um algoritmo formal para revisão de modelos CTL. Dados
modelos que satisfazem a especificação formal do sistema e uma propriedade
expressa por uma fórmula CTL, nosso algoritmo gera um conjunto de modelos
que satisfazem essa propriedade e cujas distâncias dos modelos da especificação
original são mı́nimas. Os elementos gerados como resposta podem ser vistos como
possı́veis correções à modelagem inconsistente.
Por fim, discutimos questões relacionadas ao algoritmo desenvolvido e argumentamos que algoritmos baseados na abordagem de [16], como o nosso, possuem diversas complicações quando aplicados no contexto de revisão de crenças,
o que mostra a necessidade de desenvolver uma estratégia diferente e especı́fica
ao problema da revisão de modelos.
Referências
1. Carlos E. Alchourron, Peter Gärdenfors, and David Makinson. On the logic of
theory change: Partial meet contraction and revision functions. J. Symb. Logic,
50(2):510–530, 1985.
2. Francesco Buccafurri, Thomas Eiter, Georg Gottlob, and Nicola Leone. Enhancing
model checking in verification by AI techniques. Artificial Intelligence, 112(1-2):57–
104, 1999.
3. Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri.
NuSMV: A new symbolic model verifier. In Proc. of CAV, pages 495–499. SpringerVerlag, 1999.
4. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model checking. Springer, 1999.
5. M. Finger and Renata Wassermann. Revising specifications with CTL properties
using bounded model checking. In Proceedings of the 19th Brazilian Symposium
on Artificial Intelligence (SBIA’08), pages 157–166. Springer, 2008.
6. Paulo T. Guerra. Revisão de modelos CTL. Master’s thesis, Universidade de São
Paulo, 2010.
7. Paulo T. Guerra and Renata Wassermann. Revision of CTL models. In Advances
in Artificial Intelligence – IBERAMIA 2010, volume 6433 of Lecture Notes in
Computer Science, pages 153–162. Springer Berlin / Heidelberg, 2010.
8. Paulo T. Guerra and Renata Wassermann. Belief revision on computation tree
logic. volume 3, pages 2810–2811. AAAI Press / IJCAI, 2011.
9. Andreas Herzig. Logics for belief base updating. In D. Dubois and H. Prade,
editors, Handbook of Defeasible Reasoning and Uncertainty Management, volume
Belief Change, pages 189–231. Kluwer Academic, Dordrecht, 1998.
10. Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and reasoning
about systems. Cambridge University Press, 2004.
11. Hirofumi Katsuno and Alberto O. Mendelzon. A unified view of propositional knowledge base updates. In Proc. of IJCAI’89, pages 1413–1419. Morgan Kaufmann,
1989.
12. Hirofumi Katsuno and Alberto O. Mendelzon. On the difference between updating a knowledge base and revising it. In Proc. of KR, pages 387–395. Morgan
Kaufmann, 1991.
13. Thiago C. Sousa. Revisão de modelos formais de sistemas de estados finitos. Master’s thesis, Universidade de São Paulo, 2007.
14. Thiago C. Sousa and Renata Wassermann. Handling inconsistencies in CTL modelchecking using belief revision. In Proc. of the SBMF’07, 2007.
15. Marianne Winslett. Reasoning about action using a possible models approach. In
Proc. of AAAI, pages 89–93. Morgan Kaufmann, 1988.
16. Yan Zhang and Yulin Ding. CTL model update for system modifications. Journal
of Artificial Intelligence Research, 31(1):113–155, 2008.