Lógica temporal

Origem: Wikipédia, a enciclopédia livre.
Saltar para a navegação Saltar para a pesquisa
Ambox rewrite.svg
Esta página precisa ser reciclada de acordo com o livro de estilo (desde junho de 2015).
Sinta-se livre para editá-la para que esta possa atingir um nível de qualidade superior.
Question book-4.svg
Esta página ou secção cita fontes confiáveis e independentes, mas que não cobrem todo o conteúdo, o que compromete a verificabilidade (desde junho de 2015). Por favor, insira mais referências no texto. Material sem fontes poderá ser removido.
Encontre fontes: Google (notícias, livros e acadêmico)
Ambox grammar.svg
Esta página ou secção precisa de correção ortográfico-gramatical.
Pode conter incorreções textuais, e ainda pode necessitar de melhoria em termos de vocabulário ou coesão, para atingir um nível de qualidade superior conforme o livro de estilo da Wikipédia. Se tem conhecimentos linguísticos, sinta-se à vontade para ajudar.
Translation to english arrow.svg
A tradução deste artigo está abaixo da qualidade média aceitável. É possível que tenha sido feita por um tradutor automático ou por alguém que não conhece bem o português ou a língua original do texto. Caso queira colaborar com a Wikipédia, tente encontrar a página original e melhore este verbete conforme o guia de tradução.

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 nós podemos 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 usado para se referir a um particular sistema de lógica temporal baseada em Lógica Modal, introduzida por Arthur Prior no final dos anos 50, e com importantes resultados obtidos por Hans Kamp. Subsequentemente, tem sido desenvolvida por cientistas da computação como Amir Pnueli, e lógicos.

Lógica temporal encontrou uma importante aplicação em verificação formal, onde é usada para declarar requerimentos de sistemas de hardware ou software. Por exemplo, alguém pode desejar dizer que sempre que uma solicitação é feita, 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[editar | editar código-fonte]

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á verdadeiro e falso 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 lógica temporal das demais.

Lógica temporal sempre possui a habilidade de dissertar sobre uma linha temporal. Tão 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õem um ambiente que pode vir a agir imprevisivelmente. Para continuar o exemplo, em lógicas ramificáveis podemos declarar que "existe a possibilidade que eu ficarei com fome para sempre." Nós podemos dizer também que "existe a possibilidade 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[editar | editar código-fonte]

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ã".[1]

Houve pouco desenvolvimento durante um milênio, Charles Sanders Peirce notou no seculo 19:[2]

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-6, e em 1957, publicou o livro, "Time and Modality", no qual ele introduzi-o lógica proposicional modal com dois conectivos temporais (operadores modais), F e P, correspondendo a "algum momento no futuro" e "algum momento no passado". Nesse trabalho, Prior considerou tempo como sendo linear. Em 1958, no entretanto, 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".[2][necessário esclarecer] Entre 1958 e 1959 Prior também se correspondeu com Charles Leonard Hamblin, e um numero de desenvolvimentos iniciais no campo podem ser traçados a essas correspondências, por exemplo as Implicações de Hamblin. Prior publicou seu trabalho mais maduro sobre o tópico, o livro "Past, Present and Future" em 1967. Ele morreu dois anos depois.[3]

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

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 logica ramificada que pode ser decidida com a mesma complexidade.

Operadores temporais[editar | editar código-fonte]

Lógica Temporal tem dois tipos de operadores: operadores lógicos e operadores modais[1]. Operadores lógicos são os comuns. Os operadores modais usados em Lógica Temporal Linear e Arvore lógica computacional são definidos a seguir.

Textual Simbólico Definição Explicação Diagrama
Operadores Binários
U Until (Até): detém na atual ou futura posição , e tem de manter até essa posição. Nessa posição não tem que segurar mais.
R Release(Liberar): libera se é verdade até a primeira posição em que é verdade (ou para sempre se tal posição não existir).
Operadores Unarios
N Next(Próximo): deve manter no próximo estado (X é usado como sinônimo.)
F Future(Futuro): eventualmente deve manter (em algum momento no caminho subseqüente).
G Globally(Globalmente): tem que manter todo o caminho subseqüente.
A All(Para todo): tem que segurar todos os caminhos a partir do estado atual.
E Exists(Existe): existe pelo menos um caminho a partir do atual estado onde mantém.

Símbolos Alternativos:

  • Operador R é algumas vezes denotado por V
  • O operador W é o operador fraco até: é equivalente a

Operadores Unários são formulas bem formadas sempre que B() é bem formado. Operadores Binários are são formulas bem formadas sempre que B() e C() 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.

Notas[editar | editar código-fonte]

  1. Vardi 2008, p. 153
  2. a b c Vardi 2008, p. 154
  3. 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  pp. 176-178, 210
  4. http://plato.stanford.edu/entries/logic-temporal/M
  5. Walter Carnielli; Claudio Pizzi (2008). Modalities and Multimodalities. [S.l.]: Springer. p. 181. ISBN 978-1-4020-8589-5 
  6. Sergio Tessaris; Enrico Franconi; Thomas Eiter (2009). Reasoning Web. Semantic Technologies for Information Systems: 5th International Summer School 2009, Brixen-Bressanone, Italy, August 30 - September 4, 2009, Tutorial Lectures. [S.l.]: Springer. p. 112. ISBN 978-3-642-03753-5 

Referencias[editar | editar código-fonte]

  • 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.)

Mais leitura[editar | editar código-fonte]

  • 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[editar | editar código-fonte]

Predefinição:Logica