ADDSON ARAUJO DA COSTA
IGOR LINNIK CAMARA ARAUJO
LUANA WANDECY PEREIRA SILVA
MARCOS AURÉLIO C. DOS SANTOS
ROSANA CAETANO DE FARIA MONTEIRO
SILVIO ROMERO DE AZEVEDO COSTA
 Introdução
 Histórico
 Motivação
 Estrutura de Kripke
 Caminhos
 Padrões
 LTL
 CTL*/CTL
 Expressividade
 Aplicações
 Verificação de modelos
 Conclusão
 Introdução
 Histórico
 Motivação
 Estrutura de Kripke
Tempo Linear X Tempo Ramificado
 Na lógica temporal, o tempo não é mencionado explicitamente, mas
visto como possíveis seqüências de estados associados às suas
transições.
 Estado é a descrição do sistema em um dado instante de tempo, ou seja,
os valores associados às suas variáveis naquele instante, enquanto
transição é uma relação entre dois estados.
 Tipicamente, as afirmações sobre o comportamento do sistema em um
determinado estado são feitas através de propriedades, e estas por sua
vez são expressas como fórmulas de uma linguagem de lógica temporal,
que especificam os comportamentos desejados.
 A maneira como é feita a representação do tempo nas propriedades,
isto é, de maneira linear ou ramificada, faz com que haja dois modelos
básicos de lógicas temporais: Linear Temporal Logic (LTL) e
Computation Tree Logic (CTL).
Tempo Linear
 É
Tempo Ramificado
aquele em que o  Todo o comportamento
comportamento
do
do sistema é
sistema
consiste
no
representado por uma
conjunto
de
traços
árvore computacional de
infinitos que começam
profundidade ilimitada
no estado inicial i.
cuja raiz é o estado
inicial i.
Exemplo:
 Exemplo:
 É uma lógica temporal de tempo linear que interpreta fórmulas sobre
funcionamentos do sistema, e faz a caracterização de cada caminho
linear proporcionado pelas máquinas de estados finitos.
 A lógica LTL considera que há somente um único estado sucessor, ou
seja, um único futuro possível, a cada momento do tempo.
 As fórmulas LTL são avaliadas sobre caminhos lineares, e uma fórmula
somente é considerada verdadeira em um modelo se ela é verdadeira
para todos os caminhos iniciando num dos estados iniciais daquele
modelo.
 Sintaxe:
Uma fórmula LTL sintaticamente válida é formada pelas variáveis proposicionais p1, p2, (...),
os conectivos usuais da lógica proposicional (, , ,  ), e os seguintes operadores
temporais:
o Next: X  -  é verdadeiro no próximo estado;
o Future: F  -  é eventualmente válida (em algum estado do caminho);
o Globally: G  -  é sempre válida (em todo estado no caminho);
o Until:  U  -  é verdadeira no caminho até que  seja verdadeira;
o Release:  R  - quando a ocorrência de um estado onde  é válida liberta  de o ser.
o Exists: E  -  é verdadeiro num caminho S se existe um caminho começando em um
estado S
o All: A  -  é verdadeiro para todo caminho começando no estado S.
Os conectivos são X, F e G são usados algumas vezes através dos símbolos , , ,
respectivamente.
Caminho - Um caminho em M é uma seqüência
infinita de estados s0 , s1 , s2 , ... tal que s0 ∈ I e (si ,
si+1 ∈ R para todo i ≥ 0).
Semântica - Sejam p ∈ AP uma proposição atômica,
σ caminho infinito e φ, ψ fórmulas LTL, a relação
“satisfaz”, denotada por |=, é definida por:
σ |= p
⇔
p ∈ Label(σ[0])
σ |= ¬φ
⇔
not(σ |= φ)
σ |= φ ∧ ψ ⇔
(σ |= φ) and (σ |= ψ)
σ |=Xφ
⇔ σ 1 |= φ
σ |= φUψ
⇔ ∃j ≥ 0, (σ j |= ψ and (∀0 ≤ k < j, σ k
|= φ))
Os padrões mais freqüentes são:
Ausência: quando no contexto se pretende que não ocorram
certos eventos ou estados.
Universalidade: quando se pretende que em todo o contexto
certa propriedade se verifique.
Existência: quando se pretende que uma propriedade ocorra
alguma vez no contexto.
Resposta: dentro do contexto a ocorrência de certo evento
(causa) deve ser seguida da ocorrência de outro (efeito).
Axiomas:
- Leis de distribuitividade
X (  )  X   X 
X (  )  X   X 
X 
 X 
F (  )  F   F 
Leis de distribuitividade
F 
 G 
G(  )
G   G 
G 
 F 
(  ) U  
( U )  ( U )
 U (  ) 
( U )  ( U )
- Leis de idempotência
FF 
GG 
FGF 
GFG 
 U ( U )
F
G
 GF 
 FG 
U
- Leis de expansão
F
   XF 
G
   XG 
 U     (  X ( U ))
Verificação de modelos usando LTL:
Dado um modelo M formalmente representado pela
estrutura de Kripke M = ( S, I, R, Label) e uma
fórmula LTL φ:
M |= φ se e somente se ∀s ∈ I, (∀ Caminhos(s), σ |= φ)
 LTL considera apenas um único estado
 Em meados de 80, Clarke e Emerson
 Considerar diferentes estados possíveis
 Utilizada em vários verificadores de modelos
 LTL considera apenas um único estado
 Em meados de 80, Clarke e Emerson
 Considerar diferentes estados possíveis
 Utilizada em vários verificadores de modelos
 Possibilidade de descrever MEF como uma árvore de
estados infinita
 Desdobramento de uma estrutura de Kripke em árvore
de computação infinita
 Composta por:
 Fórmulas de estados (ФS)
 Fórmulas de caminhos (ФP)
• Acrescenta a LTL, quantificadores de
caminho:
 Existencial (E)
 Universal (A)
 Eα
 É verdadeira em um estado s se existe um caminho
começando em s tal que α é verdadeira neste caminho;
 Aα
 É verdadeira em um estado s se para todo um caminho
começando em s, α é verdadeira neste caminho.
 Operadores
 X
 F
 G
 U
 Xα: é verdadeira em um caminho π, se no próximo
estado do caminho α é verdadeira
α
 Fα: é verdadeira em um caminho π, se em algum
estado no caminho α é verdadeira
α
 Gα: é verdadeira em um caminho π, se em todo estado
no caminho α é verdadeira
α
α
α
α
 αUβ: é verdadeira em um caminho π, se α é verdadeira
no caminho até que β seja verdadeira
α
α
β
 Gerada pela BNF:
 ФS ::= P | (¬ФS) | (ФS ∧ ФS) | (ФS ∨ ФS) | (ФS → ФS) | (EФP)
| (AФP)
 ФP ::= ФS | (¬ФP) | (ФP ∧ ФP) | (ФP ∨ ФP) | (ФP → ФP) |
(XФP) | (FФP) | (GФP) | (ФP U ФP)
 Dada pela definição ⊨ de CTL
 Satisfação em estado
 K ⊨s α
 Satisfação em caminho
 K ⊨π α
 K ⊨s P ⇔ P ∈ L(s)
 K ⊨s (¬α) ⇔ NOT K ⊨s α
 K ⊨s (α ∧ β) ⇔ K ⊨s α E K ⊨s β
 K ⊨s (α ∨ β) ⇔ K ⊨s α OU K ⊨s β
 K ⊨s (α → β) ⇔ SE K ⊨s α ENTÃO K ⊨s β
 K ⊨s (Eα) ⇔ Existe um caminho π a partir de s tal que
K ⊨π α
 K ⊨s (Aα) ⇔ Para todo caminho π a partir de s vale que
K ⊨π α
 K ⊨π α ⇔ se α é uma fórmula da linguagem Фs,








K ⊨π0
α
K ⊨π (¬α) ⇔ NOT K ⊨π α
K ⊨π (α ∧ β) ⇔ K ⊨π α E K ⊨π β
K ⊨π (α ∨ β) ⇔ K ⊨π α OU K ⊨π β
K ⊨s (α → β) ⇔ SE K ⊨π α ENTÃO K ⊨π β
K ⊨π (Xα) ⇔ K ⊨π1,∞ α
K ⊨π (Fα) ⇔ Existe um k ≥ 0 tal que K ⊨πk,∞ α
K ⊨π (Gα) ⇔ Para todo k ≥ 0 vale que K ⊨πk,∞ α
K ⊨π (αUβ) ⇔ Existe k ≥ 0 tal que K ⊨πk,∞ β e para todo
0 ≤ l < k vale que K ⊨πl,∞ α
 Subconjunto da CTL*
 Operador temporal precedido por quantificador de
caminho
 Semântica e operadores = CTL*
 [EX]α – existe um caminho tal que no próximo estado
vale α
α
 [AX]α – para todo caminho no próximo estado vale α
α
α
 [EF]α – existe um caminho tal que no futuro vale α
α
 [AF]α – para todo caminho no futuro vale α
α
α
α
 [EG]α – existe um caminho tal que sempre vale α
α
α
α
 [AG]α – para todo caminho vale sempre α
α
α
α
α
α
α
α
 E(αUβ) – existe um caminho tal que vale α até que vale
β
α
β
 A(αUβ) – para todo caminho vale α até que vale β
α
α
β
β
β
Existe uma discussão sobre a melhor lógica para expressar
propriedades, LTL ou CTL. Contudo, as propriedades
usualmente utilizadas na verificação de tais sistemas podem
ser expressas nas duas lógicas. Propriedades podem ser
descritas em uma lógica e não podem na outra, e vice-versa.
A maior parte das propriedades pode ser expressa tanto em
CTL quanto em LTL.
 Por exemplo,
a invertibilidade apenas pode ser
expressa em CTL.
 Propriedades existenciais não podem ser expressas na
lógica LTL. Este tipo de propriedade é muito útil na
procura de possíveis deadlocks em um sistema. Já a
lógica CTL, não é capaz de expressar algumas
propriedades de razoabilidade.
 Cada uma destas lógicas é usada em situações
diferentes, pois o uso de uma lógica ou da outra
depende do tipo de propriedade que se quer verificar.
 O quantificador existencial (E) foi incluso na lógica
CTL, mas isso não faz com que a mesma tenha um
poder de expressividade maior do que a lógica LTL. As
expressividades de LTL e CTL são incomparáveis.
 Sistema de controle de uma aeronave
 Sistema de controle de uma usina nuclear
 Sistema de controle de tráfego aéreo
 Produção em massa de produtos eletrônicos.
 Programa de Estimativa de vendas
 Simulador de investimentos
 Principal aplicação
 Exemplos:
 "será sempre o caso que...“
 será o caso que...“
 "sempre foi o caso que...“
 "foi o caso que..."
Exemplos de implementações de verificação de modelos:
SMV: Symbolic Model Verifier
SMVNu: software livre
SPIN
UPPAAL: trata de tempo-real
HYTECH: autômatos híbridos
PRISM: autômatos estocásticos
 Lógicas
temporais formalizam de modo natural
problemas computacionais.
 A verificação das especificações de modelos pode ser
feita automaticamente, através de provadores de
teorema ou checagem de modelos.











http://poesiagnosticaefilosofia.blogspot.com/2006/05/lgica-temporal-algo-descartavelfrente_12.html
http://es.wikipedia.org/wiki/L%C3%B3gica_temporal
http://pt.wikipedia.org/wiki/Regra_de_infer%C3%AAncia
http://en.wikipedia.org/wiki/Temporal_logic
http://plato.stanford.edu/entries/logic-temporal/
http://pt.wikibooks.org/wiki/L%C3%B3gica:_L%C3%B3gicas_N%C3%A3ocl%C3%A1ssicas:_Introdu%C3%A7%C3%A3o
http://books.google.com.br/books?id=ZFY3S8iinfMC&pg=PA2842&lpg=PA2842&dq=l%C3%B3gica+t
emporal&source=bl&ots=MomERmQf3j&sig=_bbRg7A7GNx8Tr8tZkvQNAgBXkQ&hl=ptBR&ei=HGB3SqCbMcmptgfVgc2WCQ&sa=X&oi=book_result&ct=result&resnum=9#v=onepage&q=l
%C3%B3gica%20temporal&f=false
http://www.itl.nist.gov/div897/sqg/dads/HTML/temporllogic.html
http://lat.inf.tu-dresden.de/teaching/ss2006/tl/
http://books.google.com.br/books?id=ghy2CMU2FIoC&pg=PA995&lpg=PA995&dq=E.+Allen+Emers
on:+Temporal+and+Modal+Logic.+In+J.+van+Leeuwen&source=bl&ots=5dMvWy4Aih&sig=XyaR2rJKHN7C4pTcbGgRioOM5o&hl=pt-BR&ei=Rox4SuBLYajtgfFh92WCQ&sa=X&oi=book_result&ct=result&resnum=1#v=onepage&q=&f=false
Slides explicativos relacionados ao tema.