Lógica Temporal

Conclusão
Os efeitos e aplicações da lógica sobre a computação se estendem sobre as mais diversas áreas da mesma, dos mais altos níveis, como inteligência artificial, aos mais baixos, como na produção dos circuitos integrados. Assim, fornece não somente uma base sólida para a fundamentação do ramo, mas também uma poderosa ferramenta para o desenvolvimento do mesmo.
Aplicações
História
Sintaxe
Semântica
Aplicações
A lógica temporal vem desempenhando importante papel nos sistemas de segurança crítica, que são aqueles sistemas onde o tempo é essencial e uma única falha pode provocar a morte de pessoas. A lógica Temporal permite a verificação da corretude desses sistemas. Alguns exemplos desses sistemas são:
Sistema de controle de uma aeronave;
Sistema de controle de uma usina nuclear;
Sistema de controle de tráfego.
Sintaxe
Semântica
Axiomas
Aplicações
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), σ "= φ)


Na Lógica LTL a validação das propriedades pode ser formulada através de um autômato de Buchi, mas devido a complexidade deste autômato, geralmente se nega a propriedade a provar e verifica se a mesma é verdadeira ou falsa.
Axiomas
Sintaxe
Semântica
Axiomas
Aplicações
Leis de expansão

F XF
G XG
U ( X ( U ))
Axiomas
Sintaxe
Semântica
Axiomas
Aplicações
Leis de idempotência

FF F
GG G
FGF GF
GFG FG
U ( U ) U
Referências

Mordechai Ben-Ari, Zohar Manna, Amir Pnueli: The Temporal Logic of Branching Time. POPL 1981: 164-176
Amir Pnueli: The Temporal Logic of Programs FOCS 1977: 46-57
Venema, Yde, 2001, "Temporal Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
E. A. Emerson and C. Lei, modalities for model checking: branching time logic strikes back, in Science of Computer Programming 8, p 275-306, 1987.
E.A. Emerson, Temporal and modal logic, Handbook of Theoretical Computer Science, Chapter 16, the MIT Press, 1990

Aplicações
História
Sintaxe
Semântica
Aplicações
A complexidade dos semicondutores implica no aumento da complexidade dos projetos, que acarretam numa dificuldade cada vez maior de desenhá-los, fazendo com que os projetistas não sejam capazes de usufruir do potencial total que a tecnologia é capaz de oferecer, devido à grande possibilidade de error.
Para contornar esses problemas, foi implementado métodos de validação do circuito, com intenção de verificar se o mesmo executa a função para a qual foi projetado, concluindo se há erros de projeto ou não. Esse tipo de processo acabou, também, se tornando complexo demais atingindo um ponto chamado "crise de validação".
Verificação formal é um processo matemático utilizado para verificar o comportamento de um modelo, e um dos métodos mais utilizados a fim de tal prática é a lógica temporal linear (LTL – Linear Temporal Logic, em inglês), onde os momentos no tempo são tratados como se houvesse um único futuro possível.
Axiomas
Sintaxe
Semântica
Axiomas
Aplicações
Leis de distribuitividade

X ( ) X X
X ( ) X X
X X
F ( ) F F
F G
G( ) G G
G F
( ) U ( U ) ( U )
U ( ) ( U ) ( U )
Axiomas
Sintaxe
Semântica
Axiomas
Aplicações
Com a adição de novos conectores temporais, novos axiomas foram acrescentados também. São eles:
Sintaxe
História
Sintaxe
Semântica
Aplicações
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:
Next: X - é verdadeiro no próximo estado;
Future: F - é eventualmente válida (em algum estado do caminho);
Globally: G - é sempre válida (em todo estado no caminho);
Until: U - é verdadeira no caminho até que seja verdadeira;
Release: R - quando a ocorrência de um estado onde é válida liberta de o ser;
Exists: E - é verdadeiro num caminho S se existe um caminho começando em um estado S
All: A - é verdadeiro para todo caminho começando no estado S.
Os conectivos X, F e G são usados através dos símbolos , , , respectivamente.




Sintaxe
História
Sintaxe
Semântica
Aplicações
Considere-se um conjunto de símbolos proposicionais π.

φ ::= T "p" ¬φ " φ/\φ " Xφ " Xφ " φ U φ

φ1 U φ2 (φ1 until φ2) - φ2 é verdadeira num instante futuro e, até esse instante, φ1 é verdadeira.

Apenas estamos a considerar o futuro.

Assumimos definidos (por abreviatura) outros conectivos proposicionais (eg. \/, , ).




Motivação
Introdução/
História
Sintaxe
Semântica
Aplicações
Propriedade 2

O semáforo tem, no máximo, uma luz acesa.
Fácil de insterpretar em lógica proposicional.


(green (¬yellow /\ ¬red) /\...

Propriedade 1

O semáforo tem pelo menos uma luz acesa.
Fácil de insterpretar em lógica proposicional.


Green \/ yellow \/ red

Propriedade 3

A seguir à luz verde acende-se a luz amarela.

????

Aplicações
História
Sintaxe
Semântica
Aplicações
VERIFICAÇÃO AUTOMATIZADA DE DESIGNS DE SEMICONDUTORES
Motivação
Introdução/
História
Sintaxe
Semântica
Aplicações
Há situações em que os atributos de "Verdadeiro" e "Falso" não bastam, e é preciso determinar se algo é "Verdadeiro no período de tempo A", ou "Falso após o evento B". Para isso, é utilizado um sistema lógico específico que inclui novos operadores para tratar dessas situações.
Em lógica, lógica temporal é qualquer sistema de regras e símbolos que serve para representar e dissertar sobre proposições qualificadas em termos de tempo.
Sintaxe
História
Sintaxe
Semântica
Aplicações
Com esta linguagem podemos escrever:




Propriedade 3

A seguir à luz verde acende-se a luz amarela

Green (X yeloow)

Ou mesmo:

Green U yellow
Introdução
Introdução/
História
Sintaxe
Semântica
Aplicações
Existem dois grandes grupos de lógica temporal:

Linear Temporal Logic (LTL): Operadores descrevem propriedades presentes em todas as possíveis trajetórias do sistema;
Full Computation Tree Logic (CTL): Operadores temporais inferem sobre diferentes trajetórias a partir de um dado estado;
Introdução
Introdução/
História
Sintaxe
Semântica
Aplicações
Seja A uma fórmula qualquer:

(i) FA – A será verdade em algum instante no futuro;
(ii) PA – A foi verdade em algum instante no passado;
(iii) GA – A será verdade em todos instantes do futuro;
(iv) HA – A foi verdade em todos instantes do passado;
Aplicações
História
Sintaxe
Semântica
Aplicações
Em LTL as fórmulas são construídas com proposições atômicas, os operadores booleanos usuais e os operadores temporais unários X (próximo), F (eventualmente) e G (sempre), e o operador temporal binário U (enquanto). Esses operadores são capazes de modelar uma computação sobre a especificação dada, sendo possível verificar seu comportamento.
7 Ferramentas para modelagem e verificação do comportamento dos semicondutores não param em LTL.
Há muitas outras abordagens lógicas possíveis para a resolução do problema, tendo, todas juntas, mostrado sua capacidade para auxiliar na continuidade da evolução da área, resolvendo problemas fundamentais para a computação
Introdução
Introdução/
História
Sintaxe
Semântica
Aplicações
Lógica Temporal é uma extensão de lógica convencional que incorpora operadores especiais para relacionar a validade das fórmulas à evolução do sistema.
Definida a partir dos seguintes operadores: G, F, H, P.
Sendo que os primitivos são G e H, e os outros podem ser introduzidos através das seguntes equivalências:
F A ¬G ¬A
P A ¬H ¬A
O termo faz menção às lógicas que buscam falar sobre o tempo. Atrelar as ideias de possibilidade e necessidade com as de tempo. Por exemplo: "Possivelmente choverá amanhã", ou "é necessário que chova amanhã".
História
Introdução/
História
Sintaxe
Semântica
Aplicações
Apesar da lógica aristotélica se preocupar quase inteiramente com a teoria de silogismo categórico, há passagens em seu trabalho que são vistas hoje como antecipações da lógica temporal, e podem implicar em uma primitiva, parcialmente desenvolvida forma de lógica modal temporal binária de primeira ordem.
Aristóteles estava particularmente preocupado com o problema dos futuros contingentes, onde ele não aceitava que o princípio da bivalência podia ser aplicado a declarações sobre eventos futuros, i.e. que nós podemos atualmente decidir se uma declaração sobre eventos futuros é verdadeira ou falsa, como por exemplo "haverá uma batalha naval amanhã".
Sintaxe
História
Sintaxe
Semântica
Aplicações
Caminho
Um caminho em M é uma sequência infinita de estados S0, S1, S2,..., tal que S0 I e ( SI, SI+1 R para todo I 0). Ou seja, é uma seqüência infinita de estados que representa uma possível execução do sistema a partir do seu estado inicial.
História
Introdução/
História
Sintaxe
Semântica
Aplicações
Arthur Prior [1914-1969]
Considerado o fundador da lógica temporal
Tense Logic - Prior acrescentou quatro operadores à lógica proposicional clássica:
F Alguma vez no fututro..."
P Alguma vez no passado..."
G Sempre no futuro..."
H Sempre no passado..."
Aristóteles [384 a.C. - 322 a.C.]

O sistema lógico de Aristóteles foi responsável pela introdução do silogismo hipotético, lógica modal temporal e lógica indutiva.
Willard V. O. Quine [1908-2000]

Quine propõe que o discurso temporal seja representado dentro do aparato clássico; na verdade, ele elimina o tempo verbal. Para isso, propôs a reescrita dos argumentos informais em simbolismo formal, por meio de uma variável "t", que varia entre épocas.
História
Introdução/
História
Sintaxe
Semântica
Aplicações
O primeiro trabalho mais amplo, rigoroso e sistematizado feito sobre o tema da lógica é o de Aristóteles. A lógica aristotélica tornou-se amplamente aceita em ciências e matemática e manteve-se em ampla utilização no Ocidente até o início do século XIX.
O sistema lógico de Aristóteles foi responsável pela introdução do silogismo hipotético, lógica modal temporal e lógica indutiva.
Na Europa, durante o final do período medieval, grandes esforços foram feitos para mostrar que as ideias de Aristóteles eram compatíveis com a fé cristã. Durante a Alta Idade Média, a lógica se tornou o foco principal dos filósofos, que se engajaram em análises lógicas críticas dos argumentos filosóficos
Introdução
Introdução/
História
Sintaxe
Semântica
Aplicações
Sistema base
Regra da necessitação: se A é teorema de K, então também o são G A e H A.
Axiomas da distribuição:
G (A B) (G A G B)
H (A B) (H A H B)
Axiomas de iteração:
A G P A
A H F A

Outros axiomas podem ser adicionados para criar novos sistemas, como é o caso da Lógica temporal linear (estendendo-a com a adição dos operadores S e U (desde e até) e retirando os operadores H e P para tratar a ideia de ordem temporal e a de que não é possível voltar no tempo).
O sistema básico de lógicas temporais, chamado Kt, é resultado de adotar-se os princípios de K tanto para G como para H, junto com dois axiomas para controlar as interações entre os operadores de passado e futuro:
Semântica
História
Sintaxe
Semântica
Aplicações
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 "=φ))
Lógica Temporal
Flávia Morales Antunes
Guilherme Soares Belo
Jean da Silva Bragamonte

Universidade Federal
do Pampa
































































Clique para editar o formato do texto do título
Clique para editar o formato do texto da estrutura de tópicos
2.º Nível da estrutura de tópicos
3.º Nível da estrutura de tópicos
4.º Nível da estrutura de tópicos
5.º Nível da estrutura de tópicos
6.º Nível da estrutura de tópicos
7.º Nível da estrutura de tópicos
Clique para editar o formato do texto do título
Clique para editar o formato do texto da estrutura de tópicos
2.º Nível da estrutura de tópicos
3.º Nível da estrutura de tópicos
4.º Nível da estrutura de tópicos
5.º Nível da estrutura de tópicos
6.º Nível da estrutura de tópicos
7.º Nível da estrutura de tópicos