Lógica clássica é boa para descrever um mundo estático, mas sistemas computacionais são dinâmicos. A lógica temporal é uma categoria de formalismos que procura descrever como as propriedades de um sistema variam com o tempo, porém sem se referir explicitamente ao tempo. As propriedades que tipicamente são verificadas com lógica temporal são:

Segurança (safety): nada de ruim irá acontecer. Ex: não há deadlock, não ocorrem violações de exclusão mútua, mensagens duplicadas não são entregues.
Vivacidade (liveness): algo de bom vai ocorrer. Ex: um programa fatalmente irá terminar, uma mensagem transmitida será corretamente recebida em algum momento futuro.
Justiça (fairness): sistemas independentes progridem. Ex: se o meio de transmissão estiver frequentemente disponível, uma entidade de protocolo no final das contas conseguirá transmitir uma mensagem.

A lógica temporal introduz operadores temporais, usados para descrever a dinâmica de sistemas ao longo do tempo. Curiosamente, o tempo não aparece explicitamente em expressões formadas com esses operadores. Para fins de nosso estudo, será considerado um tempo linear, com um único caminho de execução (a alternativa é um tempo ramificado, em que múltiplos caminhos de execução são levados em conta). Ambas abordagens pressupõem um sistema modelado como um sistema de transições com rótulos (LTS - labeled transition system), como, por exemplo, máquinas de estados finitos. Cada passo de um caminho de execução é definido por um conjunto de proposições primitivas que avaliam para verdadeiro. Exemplos de proposições são:

msg_tx: mensagem foi transmitida (msg_tx é uma variável booleana)
inCS_A: processo A está executando em uma seção crítica (inCS_A é um rótulo)
x == 0: variável x tem valor 0
proc@label: processo proc está executando linha identificada pelo rótulo label

Sendo assim, um estado S é definido pelas proposições que são verdadeiras nesse estado.

Operadores temporais

Os operadores temporais se aplicam a estados, considerando uma sequência de estados. Tomando-se as fórmulas de lógica temporal f e g:

Xf: f é verdadeiro no próximo estado (next f)
Gf: f é verdadeiro em todos os estados (always f)
Ff: f é verdadeiro em algum estado futuro (eventually f)
fUg: g é verdadeiro em algum estado futuro, e f é verdadeiro em cada estado até então (f until g)

Outra notação:

G: $\square$
F: $\diamondsuit$
X: $\bigcirc$

Dado o conjunto de proposições P, e fórmulas LTL f e g, as fórmulas LTL podem ser formadas com estas regras:

p (uma proposição $p\in P$ )
Operadores booleanos:
- $\neg f$ : not f
- $f\vee g$ : f or g
- $f\wedge g$ : f and g
- $f\implies g$ : f implies g
Operadores temporais:
- $\bigcirc f$
- $\square f$
- $\diamondsuit f$
- f U g

Uma outra forma de visualizar esses operadores temporais está ilustrada a seguir:

Algumas identidades entre fórmulas com esses operadores são:

$\square f\Leftrightarrow \neg (\diamondsuit \neg f)$ ... $\diamondsuit f\Leftrightarrow \neg (\square \neg f)$
$\square \square f\Leftrightarrow \square f$ , $\diamondsuit \diamondsuit f\Leftrightarrow \diamondsuit f$
$\diamondsuit f\Leftrightarrow trueUf$ , $\square f\Leftrightarrow \neg (trueU\neg f)$
f W g $\Leftrightarrow fUg\vee f$

Propriedades distributivas:

$\square (f\wedge g)\Leftrightarrow \square f\wedge \square g$
$\diamondsuit (f\vee g)\Leftrightarrow \diamondsuit f\vee \diamondsuit g$
$\bigcirc (fUg)\Leftrightarrow (\bigcirc f)U(\bigcirc g)$
$\bigcirc (f\vee g)\Leftrightarrow (\bigcirc f)\vee (\bigcirc g)$
$\bigcirc (f\wedge g)\Leftrightarrow (\bigcirc f)\wedge (\bigcirc g)$

LTL e Spin

O verificador spin é capaz de verificar fórmulas LTL. As proposições primitivas podem ser:

Proposição primitiva	Exemplo
expressões baseadas em variáveis globais	(x == 0)
rótulos de processos	p1@inicio (rótulo inicio do processo p1) p1[2]@inicio (rótulo inicio do processo p1 com pid 2)
variáveis locais de processos	p1:x (variável local x do processo p1) p1[2]:x (variável local x do processo p1 com pid 2)

Os operadores temporais suportados são (OBS: note a falta do operador next):

Operador LTL no Spin	Operador LTL
[]	$\square$ (always)
<>	$\diamondsuit$ (eventually)
U	U (until)
&&	$\wedge$
\|\|	$\vee$
->	$\implies$
<->	$\Leftrightarrow$
!	$\neg$ (negação)

Variáveis e funções predefinidas que podem ser úteis:

_pid: variável local que contém o PID de um processo
_last: variável global que contém o PID do processo que contém a última sentença executada
enabled(pid): função global que retorna true se existe ao menos uma sentença executável no processo identificado por pid

Para declarar fórmulas LTL em um modelo Promela, basta acrescentá-las ao final do arquivo com esta sintaxe:

ltl nome1 { formula 1}
ltl nome2 { formula 2}
...
ltl nomeN { formula N}

A geração do verificador deve ser feita com estes comandos:

spin -a modelo.pml
gcc -o pan pan.c

Por fim, a execução do verificador se faz assim:

./pan -a

Fórmulas LTL em geral

As fórmulas LTL simples, sem operadores temporais, são consideradas verdadeiras se avaliarem para VERDADEIRO no primeiro estado do modelo. Quer dizer, elas devem valer no momento em que o modelo for iniciado, e antes de qualquer sentença ser executada. Por exemplo, seja este modelo:

int n=7

active proctype teste() {
  do
  :: n > 0 -> n--
  :: n < 5 -> n++
  od
}

Nesse modelo a variável global n inicia com o valor 7, e nos estados subsequentes ela pode variar aleatoriamente entre 0 e 5. Considerem-se as seguintes fórmulas LTL:

(n == 7): esta fórmula avalia para verdadeiro, pois no primeiro estado do modelo de fato n tem o valor 7.
(n == 5): esta fórmula avalia para falso, pois no primeiro estado do modelo n tem na verdade o valor 7.

Operadores temporais

Os operadores temporais são usados para criar proposições que envolvem mais de um estado. São eles (essas figuras foram copiadas deste resumo sobre Spin e Promela).

Assim como fórmulas simples, fórmulas LTL com esses operadores são aplicadas ao estado inicial.

Considerando o exemplo da seção anterior, podem-se declarar estas fórmulas:

[] (n == 7): avalia para falso, uma vez que a variável n inicia com valor 7, mas nos estados subsequentes ela assume outros valores.
[] (n >= 0): avalia para verdadeiro, uma vez que a variável n assume valores entre 0 e 7.
<>(n == 7): avalia para verdadeiro, pois a variável n inicia com valor 7
<>(n == 5): avalia para verdadeiro, pois realmente em algum estado futuro n terá o valor 5.
<>(n == 0): avalia para falso, pois existe ao menos uma sequência de estados em que n nunca assume o valor 0 (imagine que n oscile entre 4 e 5 indefinidamente, por exemplo).

Esses operadores temporais podem ser combinados de forma a gerar fórmulas mais ricas:

Indefinidamente frequente: a proposição A é verdadeira ao menos uma vez em um ciclo

Travamento: em algum estado futuro a proposição A é verdadeira, e desse estado em diante ela é sempre verdadeira

Novamente considerando o exemplo da seção anterior, podem-se avaliar estas fórmulas:

[] <> (n != 5): avalia para verdadeiro, pois a variável n assume valores diferentes de 5 de forma indefinitamente frequente (compare isso com o resultado da fórmula <> (n == 5) vista anteriormente).
[] <> (n == 5): avalia para falso, pois a variável n, apesar de assumir o valor 5 garantidamente ao menos uma vez, pode passar a assumir valores menores que 5 de forma indefinitamente frequente.
<> [] (n < 5): avalia para falso, pois a variável n pode eventualmente assumir o valor 5.
<> [] (n < 6): avalia para verdadeiro, pois uma vez que a variável n assume o valor 5, nunca mais se torna maior que 5.

Precedência entre propriedades

Os operadores temporais não podem relacionar propriedades em diferentes estados (ou instantes). Por exemplo, pode-se desejar expressar que uma propriedade A é válida até que outra propriedade B se torne válida. Casos como esse são resolvidos com o operador U (until).

Dever-se notar que a propriedade A deve ser válida pelo menos até que B se torne verdadeira. Assim, A pode continuar válida mesmo após B se tornar verdadeira, e ainda assim a relação until ser verdadeira. Outro detalhe é que basta que B seja verdadeira uma vez para que a relação seja verdadeira.

Exemplificando esse operador com o modelo das seções anteriores, podem-se escrever estas fórmulas:

(n > 5) U (n <= 5): avalia para verdadeiro, pois no início a variável decrementa de 7 até 5, e depois seus valores ficam entre 0 e 5.
(n > 5) U (n == 5): avalia para verdadeiro, pois no início a variável decrementa de 7 até 5 (apesar de, uma vez atingido o valor 5, a variável n poder nunca mais assumir novamente esse valor).
(n == 6) U (n <= 5): avalia para falso, pois a variável n inicia com 7 (lembre que fórmulas são avaliadas a partir do primeiro estado do modelo)
<> ((n == 6) U (n <= 5)): avalia para verdadeiro, pois em algum estado futuro a variável n terá o valor 6 até que seus valores fiquem então entre 0 e 5.

Implicação entre propriedades

A relação de implicação entre propriedades expressada por A -> B significa que, se uma propriedade A for verdadeira, B também deve ser verdadeira. Por outro lado, se A for falsa, o valor de B é indiferente. Desta forma, essa relação é falsa somente se A for verdadeira e B for falsa. Para fins de recordação, a tabela verdade dessa relação e mostrada a seguir.

A	B	A -> B
falso	falso	verdadeiro
falso	verdadeiro	verdadeiro
verdadeiro	falso	falso
verdadeiro	verdadeiro	verdadeiro

A relação de implicação pode ser útil para as fórmulas LTL, pois possibilita expressá-las como se algo é verdade, outra coisa deve ser verdade, ou se algo é verdade, outra coisa deve ser verdade no futuro, entre outras possibilidades. Para exemplificar a relação de implicação, o seguinte modelo é usado:

int n = 5
bool down = true

active proctype ex2() {
  do
  :: down ->
    n--
    down = (n > 0)
  :: else ->
    n++
    down = (n == 5)
  od
}

Com base nesse modelo, algumas verificações podem ser feitas:

[] (down -> <> !down): essa fórmula avalia para verdadeiro e expressa que, sempre que o valor da variável down for verdadeiro, em algum momento futuro será falso.
[] (down -> <> !down) && [] (!down -> <> down): essa fórmula avalia para verdadeiro e expressa que o valor da variável down alterna entre verdadeiro e falso.
[]<>(!down -> <> (n==5)): avalia para verdadeiro, e expressa que sempre que down é falso, no futuro a variável n terá valor 5 (e isso acontece de forma indefinidamente frequente).
[]<>(down -> <> (n==0)): avalia para verdadeiro, e expressa que sempre que down é verdadeiro, no futuro a variável n terá valor 0 (e isso acontece de forma indefinidamente frequente).

Deve-se ter um cuidado com o uso da relação de implicação, pois ela avalia para verdadeiro se a propriedade da esquerda for falsa. Quer dizer, se a propriedade da esquerda nunca for verdadeira, então não importa se a propriedade implicada é verdadeira ou falsa. Assim, recomenda-se conferir se a propriedade da esquerda avalia para verdadeiro em ao menos uma possível execução do modelo. Isso pode ser feito com uma fórmula LTL como esta (supondo A -> B):

<> A

Isso significa: A é verdadeira no futuro, OU: não é sempre verdade que A seja falsa.

Exemplo de uso

Um primeiro exemplo pode ser aplicado ao caso de exclusão mútua entre processos. Supondo que inCS_X signifique processo X está na seção crítica, as seguintes proposições podem ser definidas:

Processos A e B nunca estão na seção crítica ao mesmo tempo:
- $\square (\neg inCS_{A}\vee \neg inCS_{B})$
Nenhum dos processos monopoliza a seção crítica:
- $\square (inCS_{A}\implies \diamondsuit \neg inCS_{A})$
- $\square (inCS_{B}\implies \diamondsuit \neg inCS_{B})$

No spin, essa verificação pode ser feita com este modelo e respectivas fórmulas LTL:

mtype { p, v };

chan sema = [0] of { mtype };

active proctype Dijkstra()
{       byte count = 1;
end:    do
        :: (count == 1) ->
                sema!p; count = 0
        :: (count == 0) ->
                sema?v; count = 1
        od
}

active proctype p1()
{       do
        :: sema?p;        /* enter */
critical: skip;           /* leave */
          sema!v;
        od
}

active proctype p2()
{       do
        :: sema?p;        /* enter */
critical: skip;           /* leave */
          sema!v;
        od
}

// Apenas um processo está em sua seção crítica por vez
ltl crit { [] (! p1@critical || ! p2@critical)}

// Nenhum processo monopoliza a seção crítica
ltl justica { [] (p1@critical -> <> ! p1@critical) && [] (p2@critical -> <> ! p2@critical)}

Atividades

1. Para o sistema descrito no modelo Promela a seguir, verifique se é garantido que o contador atinja o valor 10:

int count;
bool incr;

active proctype counter() {
  do
  :: incr && count < 10 -> 
    count++
    incr = false
  :: count == 10 -> count = 0
  od
}

active proctype env() {
  do
  :: !incr -> incr = true
  od
}

Fórmula LTL

2. Para o sistema do exercício 1, verifique se o valor do contador cont assume o valor 10 de forma cíclica.

3. Para o sistema do exercício 1, verifique também se a execução dos processos possui a propriedade da justiça: ambos os processos devem executar infinitamente frequente. Dica: lembre das variáveis e funções predefinidas do Spin.

Fórmulas LTL

4. Seja este modelo de uma chamada telefônica, em que cada estado temporal é definido pelos atributos S (estado da chamada) e T (duração):

Modelo de uma chamada: a duração máxima de chamada é dada pela constante Tmax

Verifique esse modelo quanto ao seguinte:

Uma chamada é atendida em algum momento futuro
Uma chamada atendida nunca excede a duração Tmax

5. Seja um protocolo ARQ do tipo pare-espere, em que processo p1 envia mensagens para processo p2 por um canal não confiável:

Defina sentA para expressar se processo p1 recém enviou mensagem A, e recA se processo p2 recém recebeu mensagem A.
Defina loss para expressar se canal perdeu a última mensagem

Sendo assim, verifique estas propriedades:

Se uma mensagem for transmitida, ela será recebida em algum momento
Se uma mensagem for recebida, ela foi previamente transmitida

Por fim, escreva esse modelo Promela, declare as fórmulas LTL, e verifique seu modelo.

6. Aplique a verificação com LTL aos problemas propostos aula passada ...

Modelo do transmissor para o enquadramento (podem adaptá-lo)
mtype = {flag, esc, data} chan tx = [1] of {byte} active proctype fram_tx() { int cnt inicio: tx!flag cnt = 0 do :: tx!data -> cnt++ :: tx!esc -> tx!data cnt++ :: cnt > 0 -> tx!flag goto inicio od }

PTC29008: Verificação de Protocolos: Lógica temporal

Índice

Operadores temporais

LTL e Spin

Fórmulas LTL em geral

Operadores temporais

Precedência entre propriedades

Implicação entre propriedades

Exemplo de uso

Atividades

Menu de navegação

Pesquisa