Lógica Temporal
por
Ulrich Schiel
 COPIN - Coordenação de Pós Graduação em Informática - UFPB
POR QUE
LÓGICA TEMPORAL ?
separação entre
ESPAÇO
(Geometria
(Métrica
X
x
x
TEMPO
Aritmética)
Ordem)
O QUE É O TEMPO ????
Se ninguém me perguntar, eu sei;
se o quiser explicar, ja não sei
Santo Agostinho - (354-430)
BIBLIOGRAFIA
N. Edelweiss & J. Palazzo M. de Oliveira “Modelagem de Aspectos
Temporais de Sistemas de Informação” IX Escola de Computação,
Recife, 1994
A. Galton “Temporal Logics and their Applications” Academic
Press, 1987
Z. Manna & A. Pnueli “The Temporal Logic of Reactive and
Concurrent Systems” Springer Verlag, 1991
U. Schiel “Aspectos Temporais em Sistemas de Informação”,
Relatório Técnico DSC 001/96, UFPB/DSC, 1996
O TEMPO
em sistemas de informação
Modelagem
temporal
Modelagem
comportamental
Estuda os tempos
quando eventos ocorre
ou fatos existem
Estuda as ações
e reações do sistema
aos eventos
•Bancos de Dados Temporais
•Lógica temporal
•Lógica de intervalos
•Bancos de Dados Ativos
dicotomia filosófica de visão do
TEMPO e ESPAÇO
visão absolutista (Newton)
visão relativista (Leibnitz)
o tempo (e o espaço vazio)
existem a priori.
As ’coisas’ existem no espaço
e determinam o tempo
Lógica Temporal
Calendários
Lógica do Tempo
t
passado
agora
futuro
Qual é o ‘ZERO’
do eixo do tempo da visão absolutista?
Analogamente:
aqui
Além do zero o tempo deve ter
uma ordem e uma métrica.
O conjunto T do tempo é totalmente ordenado pela
relação  (antes ou ao mesmo tempo), ou seja
t1, t2, t3T vale
 t1  t1 (reflexividade)
 t1 t2  t2t1  t1 = t2 (antisimétrica)
 t1 t2  t2t1 (linearidade)
 (t1 t2  t2t3)  t1t3 (transitividade)
Além do zero o tempo deve ter uma métrica.
Uma métrica para o conjunto T do tempo é uma função
d : TxT ->> R
que associa a cada par de elementos de T um número real
tal que, para todo t1, t2 e t3 em T, temos
d(t1,t2) = 0  t1 = t2
d(t1,t2) = d(t2,t1)
d(t1,t2) + d(t2,t3)  d(t1,t3)
Se o tempo é um conjunto discreto a métrica é dada
por uma constante associada a dois pontos adjacentes,
denominada chronon. Pode ser um segundo, uma
hora, um século, etc.
Considerações/modelos sobre o tempo:
elemento primitivo: Ponto
ou
Intervalo
Densidade: Discreto (enumerável) ou Contínuo
Espaço: Presente ou Futuro ou Passado ou Presente e Futuro
ou todos os tempos
Ordem:
Linear
ou
Lógica: Primeira Ordem
Ramificado ou Paralelo
ou
Modal
Lógica Temporal
É uma Lógica Modal
Principais operadores modais
[] P - P será sempre verdadeiro
<> P - P será verdadeiro alguma vez
() P - P será verdadeiro no próximo estado
P até Q - P será verdadeiro até Q ocorrer
P com Q - P será verdadeiro com a próxima ocorrência de
FATOS:
[] P  ~<> ~P
[] P  ()[] P
P até Q  Q com (P  Q)  ()<> Q
EXEMPLOS
1. Todo dia dou um passeio no parque
2. Alguma noite irei busca-la
3. Vou chorar até você voltar para, então, parar
Então temos:
1. [](P  <>Q) ??
Seja: P = é dia
Q = passeio no parque
R = vou buscar você
S = estou chorando
T = sua volta
[] (P  ~(~Q até ~P ))
2. <> (~P  R )
3. S até T  (T  ()~S))
T1: []p  ~<>~p
AXIOMAS
T2: <>p  ~[]~p
T3: ()~p  ~()p
T4: p  <>p
T5: []p  p
T6: <>[]p  []<>p
Variantes da Lógica Temporal
Lógica Temporal com passado
[+] P - sempre no futuro
[-] P - sempre no passado
<+> P - Alguma vez no futuro
<-> P - alguma vez no passado
Lógica Temporal ramificada
T - em todo futuro
A - em algum futuro
EXEMPLO: o programa pode dar um deadlock (D). Neste caso,
vou interromper o sistema (IS)
A(D  () IS)
Ou melhor: A(D)  (D  () IS)
Aplicações:
INTELIGÊNCIA ARTIFICIAL
Raciocínio temporal
[](trovão  (-) raios) “todo trovão é precedido por raios”
Processamento de linguagem natural
(Termos quando, enquanto, ontem, sempre, depois, conjugação
dos verbos, ..)
PROGRAMAÇÃO
programação concorrente
verificação de programas
corretude (safety)
P  []Q
vitalidade (liveness) P  <>Q
precedência
P  Q com R
BANCOS DE DADOS
Consistência Temporal
Um carro deve ir para a revisão de 3 em 3 anos:
[](revisão(c) = ano-atual - 3  <>(revisão(c) antes fim(ano-atu
1) salários não podem baixar
temSalário(x, s)  [+] ( s’(temSalário(x,s’) s s’) )
2) quem ja foi empregado, nunca mais pode ser admitido
<-> ( EXy(trabalhaPara(x,y)))  ~EXECUTABLE(admitir(x) )
BANCOS DE DADOS
Consistência Temporal
Um carro deve ir para a revisão de 3 em 3 anos:
[](revisão(c) = ano-atual - 3  <>(revisão(c) antes fim(ano-atu
Bancos de dados Temporais
Teoria Geral de Ações e Tempo de Allen
1) Entidades e relacionamentos vale(p,I)   I’  I (vale(p, I’)
2) Eventos (longos) ocorre(E, I)   I’  I (~ocorre(E, I’))
3) Processos:
ocorrendo(P, I)   I’  I (ocorrendo(p, I’)
EXEMPLOS: a chuva de ontem (evento) - ontem choveu (processo)
Lógica de Intervalos de Allen
Dados dois intervalos I e J, vale um dos predicados
BEFORE(I,J)
MEETS(I,J)
OVERLAP(I,J)
BEGIN(I,J)
DURING(I,J)
EQUIVALENT(I,J)
END(I,J)
Modelagem Comportamental
Lógica Dinâmica:
[programa] pós-condição
Linguagem:
Programas: P, Q, ...
Proposições: p, q, r, ...
pq 
p  são proposições
<P>p 
P::Q
P Q
P*
p?




são programas
Definição: [P]p def <P>p
“sempre que P terminar, p é verdadeiro”