Temporal

L´ogica Temporal
Manuel Alcino Cunha
Departamento de Inform´ atica Universidade do Minho

2005/06

L´ ogica Temporal

Motiva¸c˜ ao Motiva¸c˜ao

Como j´a vimos, existem v´arios tipos de propriedades desej´aveis num sistema concorrente:
Seguran¸ca “Nada de mau poder´a acontecer!”
Anima¸c˜ao “Eventualmente algo de bom ir´a acontecer!”
Em rela¸c˜ao `as propriedades de seguran¸ca j´a sabemos verificar uma subclasse muito simples de propriedades, designadas invariantes: “o sistema nunca atinge um estado de erro”.
Mas como expressar e verificar propriedades se seguran¸ca como “o sistema n˜ao pode reiniciar sem que antes o bot˜ao de reset seja pressionado”?

Manuel Alcino Cunha

L´ ogica Temporal

L´ ogica Temporal

Motiva¸c˜ ao Motiva¸c˜ao
Tamb´em j´a sabemos verificar algumas propriedades de anima¸c˜ao, como por exemplo a invertibilidade.
Mas como expressar e verificar propriedades de anima¸c˜ao como “sempre que o bot˜ao de reset ´e pressionado o sistema ser´a reiniciado”?
Embora o tempo n˜ao seja mencionado explicitamente, estas propriedades restringem as execu¸c˜oes v´alidas do sistema estabelecendo ordens e rela¸c˜oes causais entre ocorrˆencias de estados. A complexidade destas rela¸c˜oes exige um formalismo de especifica¸c˜ao adequado: a l´ogica temporal.
Nesta l´ogica temos operadores modais para exprimir propriedades como: “uma proposi¸c˜ao ´e sempre v´alida”, “uma proposi¸c˜ao ´e eventualmente v´alida”, . . .
Manuel Alcino Cunha

L´ ogica Temporal

L´ ogica Temporal

Motiva¸c˜ ao Motiva¸c˜ao
Na l´ogica temporal o tempo n˜ao ´e mencionado explicitamente, mas visto como poss´ıveis sequˆencias de estados.
Para verificar a validade de uma f´ormula ´e necess´ario saber quais as sequˆencias de estados (caminhos ou tra¸cos) poss´ıveis num determinado sistema.
A l´ ogica temporal ´e orientada aos estados: a sequˆencia de ac¸c˜oes que originou um dado caminho ´e irrelevante.
Tamb´em temos que saber qual ´e o objecto de discurso: quais as proposi¸c˜oes at´omicas da