Lógica temporal

MATHEUS MÜLLER BORGES
PAMELA BRUNH CARDOSO
RAFAEL BONA

Lógica Temporal

Trabalho apresentado como requisito parcial para obtenção de aprovação na disciplina de Lógica Aplicada à Computação, no curso de Engenharia de Computação, na Universidade Federal de Santa Catarina.
Prof. Silvia Mangili

1. INTRODUÇÃO
Uma Lógica Temporal é um sistema lógico capaz de raciocinar e analisar proposições sobre fatos e eventos que ocorrem ao longo do tempo. As Lógicas Temporais são lógicas modais que estendem a lógica clássica pela introdução de novos operadores, de modo a expressar eventos no tempo (passado, presente e futuro). No caso da Lógica Temporal Proposicional Linear, PLTL, os vários mundos possíveis são vistos como momentos de uma linha do tempo.
Embora haja registros históricos do raciocínio sobre o tempo datando da antiguidade clássica, desde reflexões filosóficas por Aristóteles (Ohrs 95), a primeira definição formal de Lógica Temporal, baseada em lógica modal, deve-se a Arthur Norman Prior, no ano de 1957, que batizou seu sistema de Tense Logic (“Lógica dos Tempos Verbais”) (Prio 57).
O objetivo da lógica temporal é sistematizar o raciocínio com proposições que têm um aspecto temporalizado.

2. TIPOS DE LÓGICA TEMPORAL
A Lógica Temporal pode ser classificada conforme as características do modelo de tempo por ela adotado. Quanto à ordem usada para representar a linha do tempo:
Linear: A linha do tempo é uma ordem linear sobre a qual cada momento possui um único sucessor. Uma estrutura de uma lógica temporal linear é comumente representada por uma reta, onde os pontos dessa reta são momentos no tempo (Figura 2.1).
Não-linear: A linha do tempo é uma ordem parcial, onde cada momento pode possuir vários sucessores. Também chamada de ramificada. É conveniente representar estruturas em uma lógica temporal não-linear como árvores ordenadas no sentido da raiz às folhas e pontos sobre os ramos