Lógica temporal

Em lógica, lógica temporal é qualquer sistema de regras e símbolos para representar e dissertar sobre proposições qualificadas em termos de tempo. Em lógica temporal, pode-se então expressar sentenças como "Eu estou sempre com fome", "Eu eventualmente estarei com fome" ou "Eu estarei com fome até eu comer algo". Lógica temporal é algumas vezes também usada para se referir a um sistema particular de lógica temporal baseada em lógica modal, introduzida por Arthur Prior no final da década de 1950; e com importantes resultados obtidos por Hans Kamp. Subsequentemente, tem sido desenvolvida por cientistas da computação, como Amir Pnueli; e lógicos.

Importância

A lógica temporal tem uma aplicação importante em verificação formal, em que é usada para declarar requerimentos de sistemas de hardware ou software. Por exemplo, alguém pode desejar dizer que sempre que uma solicitação é feita, o acesso ao recurso é eventualmente garantido, mas nunca será garantido a dois solicitantes simultaneamente. Uma declaração desse tipo pode ser expressada convenientemente em lógica temporal.

Motivação

Considere a declaração: "Eu estou com fome". Embora seu significado seja constante em relação ao tempo, o valor-verdade da declaração pode variar com o momento. Algumas vezes, a declaração é verdadeira; e algumas vezes é falsa, mas nunca será verdadeira e falsa ao mesmo tempo. Em lógica temporal, declarações podem ter um valor-verdade que variam com o tempo. Contraste isso com lógica atemporal, que só pode discutir declarações cujo valor-verdade é constante independente do tempo. Esse tratamento de valores-verdade ao longo do tempo diferencia a lógica temporal das demais.

Esse conceito sempre possui a habilidade de dissertar sobre uma linha temporal. As chamadas lógicas temporais lineares estão restringidas a esse tipo de dissertação. Lógicas ramificáveis, entretanto, podem dissertar sobre múltiplas linhas temporais. Isso pressupõe um ambiente que pode vir a agir imprevisivelmente. Para continuar o exemplo, em lógicas ramificáveis, podemos declarar que "existe a possibilidade de que eu ficarei com fome para sempre". Nós podemos dizer também que "existe a possibilidade de que eventualmente eu não estarei mais com fome." Se nós não sabemos se eu serei ou não alimentado, essas declarações são ambas verdadeiras algumas vezes.

História

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 pudesse ser aplicado a declarações sobre eventos futuros, pois nós podemos atualmente decidir se uma declaração sobre eventos futuros é verdadeira ou falsa, como por exemplo, "haverá uma batalha naval amanhã".

Houve pouco desenvolvimento durante um milênio. Charles Sanders Peirce notou, no século XIX:

“ Tempo tem sido geralmente considerado pelos lógicos o que se chama de questão 'extra lógica'. Eu nunca partilhei dessa opinião. Mas eu pensei que lógica ainda não havia atingido o estado de desenvolvimento o qual a introdução de modificações temporais de suas formas não resultaria em grande confusão; e ainda penso bastante dessa forma. ”

Arthur Prior estava preocupado com a questão lógica de livre arbítrio e predestinação. De acordo com sua esposa, a primeira vez que ele considerou formalizar lógica temporal foi em 1953. Ele deu palestras sobre o tópico na Universidade de Oxford, em 1955-1956; e em 1957, publicou o livro Time and Modality, no qual ele introduziu lógica proposicional modal com dois conectivos temporais (operadores modais), F e P, correspondendo a "algum momento no futuro" e "algum momento no passado", respectivamente. Nesse trabalho, Prior considerou tempo como sendo linear. Em 1958, no entanto, ele recebeu uma carta de Saul Kripke, que apontou que essa suposição era talvez injustificada. Num desenvolvimento que prenunciava um outro similar em ciência da computação, Prior tomou o fato em consideração; e desenvolveu duas teorias de tempo ramificado, as quais ele chamou de "Ockhamist" e "Peircean". Entre 1958 e 1959, Prior também se correspondeu com Charles Leonard Hamblin; e um número de desenvolvimentos iniciais no campo podem ser traçados a essas correspondências, como as "Implicações de Hamblin", por exemplo. Prior publicou seu trabalho mais maduro sobre o tópico, o livro Past, Present and Future, em 1967. Ele morreu dois anos depois.

Os operadores binários temporais "desde" e "até" foram introduzidos por Hans Kamp, em sua tese de Ph.D em 1968, que também possui um importante resultado relacionando logica temporal com logica de primeira ordem - um resultado hoje conhecido como Teorema de Kamp.

Dois candidatos iniciais em verificações formais foram "Lógica temporal linear" (uma lógica de tempo linear, por Amir Pnueli); e "Árvore lógica computacional" (uma lógica ramificada, por Zohar Manna e Amir Pnueli). Um formalismo quase equivalente ao de ALC foi sugerido em torno do mesmo tempo por EM Clarke e EA Emerson. O fato que a segunda lógica pode ser decidida mais eficientemente que a primeira não reflete em lógicas ramificadas e lineares em geral, como tem sido discutido algumas vezes. De preferência, Emerson e Lei mostram que qualquer lógica linear pode ser estendida para a lógica ramificada, que pode ser decidida com a mesma complexidade.

Operadores temporais

A lógica temporal tem dois tipos de operadores: operadores lógicos e operadores modais. Operadores lógicos são os comuns. E os operadores modais usados em lógica temporal linear e árvores lógicas computacionais são definidos a seguir:

Textual	Simbólico	Definição	Explicação	Diagrama
Operadores binários
$\phi$ U $\psi$	$\phi ~{\mathcal {U}}~\psi$	${\begin{matrix}(B\,{\mathcal {U}}\,C)(\phi )=\\(\exists i:C(\phi _{i})\land (\forall j<i:B(\phi _{j})))\end{matrix}}$	Until (Até): $\psi$ detém na atual ou futura posição; e $\phi$ tem de manter até essa posição. Nessa posição, $\phi$ não tem que segurar mais.
$\phi$ R $\psi$	$\phi ~{\mathcal {R}}~\psi$	${\begin{matrix}(B\,{\mathcal {R}}\,C)(\phi )=\\(\forall i:C(\phi _{i})\lor (\exists j<i:B(\phi _{j})))\end{matrix}}$	Release (Liberar): $\phi$ libera $\psi$ se $\psi$ é verdade até a primeira posição em que $\phi$ é verdade (ou para sempre, se tal posição não existir).
Operadores unários
N $\phi$	$\bigcirc \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	Next (Próximo): $\phi$ deve manter no próximo estado (X é usado como sinônimo).
F $\phi$	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )$	Future (Futuro): $\phi$ eventualmente deve manter (em algum momento no caminho subsequente).
G $\phi$	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	Globally (Globalmente): $\phi$ tem que manter todo o caminho subsequente.
A $\phi$	$\forall \phi$	${\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}$	All (Para todo): $\phi$ tem que segurar todos os caminhos a partir do estado atual.
E $\phi$	$\exists \phi$	${\begin{matrix}({\mathcal {E}}B)(\psi )=\\(\exists \phi :\phi _{0}=\psi \land B(\phi ))\end{matrix}}$	Exists (Existe): existe pelo menos um caminho a partir do atual estado onde $\phi$ mantém.

Símbolos alternativos:

• O operador R é algumas vezes denotado por V;
• O operador W é o operador fraco até: $fWg$ é equivalente a $fUg\lor Gf$.

Operadores unários são fórmulas bem formadas sempre que B($\phi$) é bem formado. E operadores binários são fórmulas bem formadas sempre que B($\phi$) e C($\phi$) forem bem formados.

Em algumas lógicas, alguns operadores não podem ser expressados, Por exemplo, o operador N não pode ser expressado em lógica temporal de ações.

Bibliografia

• 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
• Moshe Y. Vardi (2008). «From Church and Prior to Property Specification Language». In: Orna Grumberg, Helmut Veith. 25 years of model checking: history, achievements, perspectives. [S.l.]: Springer. ISBN 978-3-540-69849-4  preprint Perspectiva histórica sobre como ideias aparentemente díspares se uniram em ciência da computação e engenharia. (A referência a Church é a um fato pouco conhecido de 1957, em que ele propôs uma maneira de realizar a verificação de hardware).
• Peter Øhrstrøm; Per F. V. Hasle (1995). Temporal logic: from ancient ideas to artificial intelligence. [S.l.]: Springer. ISBN 978-0-7923-3586-3 

Ligações externas

• Stanford Encyclopedia of Philosophy: "Temporal Logic"— por Anthony Galton.
• Temporal Logic — por Yde Venema, descrição formal da sintaxe e semântica, questões de axiomatização. Tratando também os operadores temporais diádicos de Kamp (desde, até).
• Notes on games in temporal logic — por Ian Hodkinson, incluindo uma descrição formal da lógica temporal de primeira ordem.
• CADP - provides generic model checkers for various temporal logic
• PAT é um poderoso verificador de modelo gratuito, verificador LTL, simulador e verificador de refinamento para CSP e suas extensões (com variável compartilhada, matrizes, ampla gama de imparcialidade).