Lógica Temporal

Na Lógica, Lógica Temporal é qualquer sistema de regras e símbolos para representar, e argumentar sobre, proposições qualificadas em relação ao tempo. Em uma lógica temporal podemos representar afirmações como " Eu estou sempre com fome", "Eventualmente estarei com fome ", ou "Eu estarei com fome até eu comer algo ". Lógica temporal é as vezes usada para se referir à lógica tensa, um tipo particular de um sistema baseado na Lógica modal de lógica temporal introduzida por Arthur Prior no fim dos anos 50, e resultados importantes foram obtidos por Hans Kamp. Subsequentemente foi mais desenvolvida por cientistas da computação, notavelmente Amir Pnueli, e lógicos.

Lógica temporal achou uma importante aplicação na verificação formal, onde isso é usado para afirmar requerimentos de hardware ou sistemas de software. Por exemplo, alguém que deseja dizer que quando uma solicitação é feita, o acesso ao recurso é eventualmente dado, porém ele nunca é dado para dois solicitantes ao mesmo tempo. Certa afirmação pode ser facilmente representada na lógica temporal.

Motivação

Considere a afirmação: "Estou com fome" mesmo que seu significado é constante em tempo, o valor verdade da afirmação pode variar com o tempo. As vezes a afirmação é verdadeira, e as vezes a afirmação é falsa, porém a afirmação nunca é verdadeira e falsa ao mesmo tempo. Na lógica temporal, afirmações podem ter valor verdade que pode variar com o tempo. Em contraste à uma lógica atemporal, na qual só pode discutir afirmação que seu valor verdade é constante no tempo. Esse tratamento de valores verdades sobre o tempo diferencia lógica temporal de lógica verbal computacional.

Lógica temporal sempre tem a habilidade de argumentar sobre uma linha do tempo. As lógicas de tempo linear são restritas a esse tipo de argumentação. Lógicas de ramificação, contudo, pode argumentar sobre várias linhas do tempo. Isso pressupõe um ambiente que pode agir imprevisivelmente. Para continuar o exemplo, em uma lógica de ramificação podemos afirmar que "existe uma possibilidade que Eu ficarei com fome para sempre." Nós também podemos afirmar que "existe uma possibilidade que eu já não estou com fome." Se nós sabemos ou não Eu nunca vou me alimentar, essas afirmações são verdadeiras ao mesmo tempo algumas vezes.

História

Embora a lógica de Aristóteles é quase inteiramente preocupada com a teoria do silogismo, existem partes do seu projeto que agora estão sendo vistas como antecipação da lógica temporal, e que podem implicar numa primitiva, parcialmente desenvolvida forma da lógica de primeira ordem temporal modal binária. Aristóteles estava particularmente preocupado com o problema de contingentes futuros, onde ele não pode aceitar que o principio da bivalência se aplica à afirmações sobre eventos futuros , que é que podemos atualmente decidir se uma afirmação sobre eventos futuros é verdadeira ou falsa , como "amanha ocorrerá uma batalha marinha".

Houve pouco desenvolvimento durante milênios, Charles Sanders Peirce percebeu no seculo 19 :

“ Tempo foi usualmente considero por lógicos ser considerado o que é chamado de uma questão que foge da lógica. Eu nunca compartilhei essa opinião. Porém, eu pensei que a logica ainda não chegou no estado de desenvolvimento no qual a introdução de modificadores temporais de suas formas não resultaria em uma grande confusão; e eu estou muito desse modo de pensar ainda. ”

Arthur Prior estava preocupado sobre questões filosóficas de Livre arbítrio e predestinação. De acordo com sua esposa, ele primeiramente considerou formalizar a lógica temporal em 1953. Ele deu aulas sobre o tópico na Universidade de Oxford em 1955-6, e em 1957 publicou um livro, Time and Modality, no qual ele introduziu a lógica modal proposicional com dois conectivos temporais ([operador modal]|[operadores modais]]), F e P, correspondendo à "em algum momento no futuro" e "em algum momento no passado". Nesse trabalho antigo, Prior considerou tempo sendo linear. Em 1958 contudo, ele recebeu uma letra de Saul Kripke, que apontou que sua suposição talvez fosse não garantido. Em um desenvolvimento que precedeu um similar na ciência da computação , Prior tomou o conselho, e desenvolveu duas teorias de ramificação de tempo , na quais ele chamou de "Ockhamist" e "Peircean". Entre 1958 e 1965 Prior também correspondeu com Charles Leonard Hamblin, e uma série de desenvolvimentos iniciais no campo podem ser atribuídos à essa correspondência , por exemplo as implicações de Hamblim. Antes de morrer publicou seu trabalho mais maduro sobre o tópico , o livro Past, Present, and Future em 1967. Ele morreu dois anos depois.

Os operadores temporários binários Since e Until foram introduzidos por Hans Kamp na sua tese de doutorado em 1968, que também contia um importante resultado relacionando lógica temporal com lógica de primeira ordem—resultado hoje conhecido por Teorema de Kamp.

Dois primeiros candidatos em verificações formais foram Lógica temporal linear (uma lógica linear temporal por Amir Pnueli) e Árvore lógica computacional, uma lógica de ramificação de tempo por Mordechai Ben-Ari, Zohar Manna e Amir Pnueli. Um formalismo equivalente à CTL foi sugerido ao redor do mesmo tempo por E.M. Clarke e E.A. Emerson. O fato que a segunda logica pode ser decidida de forma mais eficaz não significa que a primeira não reflete sobre ramificação e logicas lineares no geral, como algumas vezes foi argumentado. Em vez disso, Emerson e Lei mostraram que qualquer logica linear pode ser estendida à uma logica de ramificação que pode ser decidida com a mesma complexidade.

Operadores temporais

Lógica temporal tem dois tipos de operadores: operadores lógicos e operadores modais [1]. Operadores lógicos são normalmente dependentes dos valores verdades ($\neg ,\lor ,\land ,\rightarrow$). Os operadores modais usados na lógica linear temporal e árvore lógica computacional são definidos a seguir.

Testual	Simbolico	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: $\psi$ mantém a atual ou uma posição futura, e $\phi$ tem que manter até aquela posição. Naquela posição $\phi$ não tem que manter 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: $\phi$ solta $\psi$ se $\psi$ é verdadeiro até a primeira posição na qual $\phi$ é verdade (ou para sempre se certa posição não existe).
Operadores unários
N $\phi$	$\bigcirc \phi$	${\mathcal {N}}B(\phi _{i})=B(\phi _{i+1})$	Next: $\phi$ tem que se manter até o próximo estado. (X é usado como sinônimo.)
F $\phi$	$\Diamond \phi$	${\mathcal {F}}B(\phi )=(true\,{\mathcal {U}}\,B)(\phi )$	Future: $\phi$ eventualmente tem que manter (em algum lugar no caminho subsequente).
G $\phi$	$\Box \phi$	${\mathcal {G}}B(\phi )=\neg {\mathcal {F}}\neg B(\phi )$	Globally: $\phi$ tem que se manter em todo caminho subsequente.
A $\phi$	$\forall \phi$	${\begin{matrix}({\mathcal {A}}B)(\psi )=\\(\forall \phi :\phi _{0}=\psi \to B(\phi ))\end{matrix}}$	All: $\phi$ tem que se manter em 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 pelo menos um caminho a partir do estado atual onde$\phi$ se mantêm.

Símbolos alternativos:

• Operador R é as vezes denotado por V
• O operador W é o fraco até operador: $fWg$ é equivalente à $fUg\lor Gf$

Operadores unários são Formulas bem formadas quando B($\phi$) for bem formado. Operadores binários são formulas bem formadas quando B($\phi$) e C($\phi$) são bem formados.

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

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
• Moshe Y. Vardi (2008). «From Church and Prior to PSL». In: Orna Grumberg, Helmut Veith. 25 years of model checking: history, achievements, perspectives. [S.l.]: Springer. ISBN 978-3-540-69849-4  preprint Historical perspective on how seemingly disparate ideas came together in computer science and engineering. (The reference to Church is to a little known 1957 in which he proposed a way to perform hardware verification.)

Leitura mais profunda

• 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 

Links externos

• Stanford Encyclopedia of Philosophy: "Temporal Logic" -- by Anthony Galton.
• Temporal Logic by Yde Venema, formal description of syntax and semantics, questions of axiomatization. Treating also Kamp's dyadic temporal operators (since, until)
• Notes on games in temporal logic by Ian Hodkinson, including a formal description of first-order temporal logic
• CADP - provides generic model checkers for various temporal logic
• PAT is a powerful free model checker, LTL checker, simulator and refinement checker for CSP and its extensions (with shared variable, arrays, wide range of fairness).