Lógica Temporal Linear (LTL)

• Interpretar uma fórmula LTL como uma afirmação sobre um único caminho infinito por uma estrutura de Kripke.
• Usar os quatro operadores temporais centrais (□, ◇, ○ e 𝖴) para enunciar propriedades de segurança e de vivacidade com precisão.
• Distinguir propriedades de segurança (nada de ruim acontece) de propriedades de vivacidade (algo bom acaba acontecendo).
• Explicar concretamente o que é um rastro de contraexemplo em forma de laço (lasso), por que ele é a testemunha característica de uma afirmação de vivacidade falsa e por que contraexemplos de segurança têm outra cara.
• Traduzir requisitos informais, como exclusão mútua e requisição-resposta, em fórmulas LTL sobre proposições atômicas rotuladas.

transition-systems-and-kripke-structures forneceu o objeto semântico (estados rotulados com proposições atômicas, conectados por uma relação de transição), mas parou antes de uma linguagem para enunciar propriedades sobre os caminhos por essa estrutura. Alguns dos requisitos mais importantes de software e hardware não são afirmações sobre um único estado final; "toda requisição acaba sendo respondida" e "o alarme nunca soa enquanto a porta está fechada" são ambas afirmações sobre um rastro de execução inteiro, potencialmente ilimitado, e nenhuma delas pode ser enunciada como uma pós-condição comum de lógica de Hoare, que só fala do estado ao final de um comando que termina.

A Lógica Temporal Linear é construída especificamente para preencher essa lacuna: ela é uma lógica de caminhos, o que significa que toda fórmula é interpretada em relação a uma única sequência de estados, linear e infinita, que se desenrola no futuro; exatamente o formato que os rastros produzidos por programas de longa duração, sistemas reativos e escalonadores naturalmente têm, e exatamente o formato que um model checker explora quando percorre uma estrutura de Kripke procurando um caminho que viole alguma propriedade. A palavra "linear" no nome faz um trabalho real e vale guardá-la desde já, porque ctl-and-branching-time-logic, o próximo conceito, introduz uma lógica genuinamente diferente, construída em torno de futuros que se ramificam em vez de futuros lineares, e o contraste entre as duas só faz sentido quando o compromisso linear da LTL está claro.

As duas fontes âncora por trás do aparato formal deste conceito dividem o trabalho de forma natural: o verbete da Stanford Encyclopedia of Philosophy sobre lógica temporal fornece os operadores e sua semântica precisa, remontando a trabalhos originalmente motivados por questões filosóficas sobre tempo e modalidade; o model checking LTL on-the-fly do SPIN mostra exatamente os mesmos operadores usados de forma concreta e prática, checando propriedades reais de sistemas concorrentes ao buscar em estruturas de Kripke caminhos que violem uma fórmula LTL.

A visão de caminho

Uma fórmula LTL é sempre interpretada sobre um único caminho infinito: uma sequência de estados s0, s1, s2, ... em que cada s(i+1) segue s(i) pela relação de transição de alguma estrutura de Kripke subjacente. Em cada posição ao longo desse caminho, cada proposição atômica é simplesmente verdadeira ou falsa, exatamente como a função de rotulagem do conceito anterior especifica. Os operadores temporais são o que permite a uma fórmula alcançar, a partir da posição atual, posições posteriores do mesmo caminho; sem eles, uma fórmula só poderia descrever o único estado em que é avaliada, sem nenhum jeito de dizer algo sobre o que vem depois.

Operadores centrais

Quatro operadores carregam quase todo o peso expressivo de que a LTL precisa para as propriedades que importam a esta disciplina. □ P (lido "sempre P", às vezes escrito G P) vale em uma posição exatamente quando P vale nessa posição e em toda posição posterior do caminho; uma afirmação sobre todo o futuro restante, sem nenhuma exceção permitida ao longo dele. ◇ P (lido "eventualmente P", às vezes escrito F P) vale em uma posição exatamente quando P vale nessa posição ou em alguma posição posterior; uma afirmação existencial sobre o futuro, satisfeita ao encontrar ao menos um ponto, por mais distante que seja, em que P se torna verdadeiro. ○ P (lido "próximo P", às vezes escrito X P) vale em uma posição exatamente quando P vale na posição imediatamente seguinte do caminho, e só nela; o único operador dos quatro que avança exatamente um passo, e não uma distância ilimitada. P 𝖴 Q (lido "P até Q") vale em uma posição exatamente quando Q acaba valendo em alguma posição atual ou posterior, e P vale em toda posição estritamente anterior a ela; crucialmente, esse operador exige que Q de fato aconteça em algum momento, então P 𝖴 Q é uma afirmação estritamente mais forte que apenas "P vale até que, se acontecer, Q ocorra".

Segurança e vivacidade

Quase toda propriedade com que esta disciplina lida, uma vez traduzida para LTL, cai em um de dois formatos amplos, e reconhecer qual formato um requisito tem muitas vezes é o passo mais útil para acertar sua fórmula LTL de primeira. Uma propriedade de segurança (safety) diz que nada de ruim acontece: seu formato natural em LTL é □ ¬bad, para o que quer que bad nomeie como condição indesejada, e sua violação é sempre testemunhada ao chegar à condição ruim em algum ponto finito, depois do qual nada mais sobre o caminho importa. Uma propriedade de vivacidade (liveness) diz que algo bom acaba acontecendo: seu formato natural envolve ◇ em algum lugar, muitas vezes aninhado dentro de um □, como em □ (request → ◇ acknowledge), e sua violação é um tipo de fato fundamentalmente diferente: exige que a coisa boa nunca aconteça, até o infinito, o que é uma afirmação sobre toda a cauda ilimitada do caminho, e não sobre algum prefixo finito dele. Muitos requisitos reais genuinamente importantes são conjunções dos dois formatos ao mesmo tempo ("requisições nunca são duplicadas, e toda requisição acaba sendo concluída" junta uma metade de segurança com uma metade de vivacidade em uma única especificação), e cada metade, em geral, precisa ser checada por um tipo diferente de argumento.

Contraexemplos

A assimetria entre propriedades de segurança e de vivacidade, apresentada acima no nível do formato das fórmulas, aparece com a mesma nitidez no que um contraexemplo de cada uma de fato é. Uma violação de segurança é testemunhada por um prefixo ruim finito: alguma sequência finita de transições que chega a um estado em que a condição proibida vale; uma vez alcançado esse estado, a violação já está completa, e nada sobre como o caminho continua muda esse fato, então um rastro finito basta totalmente como contraexemplo. Uma violação de vivacidade é um tipo de objeto genuinamente diferente e, à primeira vista, contraintuitivo: como a afirmação violada é "a coisa boa acaba acontecendo, por mais longe que seja", um contraexemplo precisa demonstrar que a coisa boa nunca acontece, o que um rastro finito sozinho não consegue fazer; como um prefixo finito provaria que nada de bom aparece depois dele, até o infinito? A solução padrão é o chamado laço (lasso): um prefixo finito de transições que leva a um ciclo (um retorno a um estado já visitado antes no rastro) de modo que o evento bom prometido nunca ocorre em nenhum ponto desse ciclo que se repete. Como o ciclo se repete para sempre depois de entrar nele, o caminho formado por seguir o prefixo e depois dar voltas no ciclo indefinidamente é um caminho infinito genuíno pelo modelo, e, como o evento bom nunca aparece em nenhum ponto do ciclo, ele nunca aparece em nenhum ponto desse caminho infinito; e é exatamente isso que é preciso para testemunhar uma violação de vivacidade de forma concreta e finita, exibindo um objeto finito (prefixo mais ciclo) que representa um caminho infinito ruim, em vez de tentar escrever o caminho infinito diretamente.

Exclusão mútua

Sejam c1 e c2 proposições atômicas que significam "o processo 1 está na sua seção crítica" e "o processo 2 está na sua seção crítica", respectivamente. A propriedade de segurança de exclusão mútua se escreve □ ¬(c1 ∧ c2): em todo ponto ao longo do caminho, não é o caso de os dois processos estarem críticos ao mesmo tempo. Isso se lê exatamente como pretendido ("sempre, não os dois") e, sendo uma propriedade de segurança, sua violação é testemunhada ao encontrar um único estado, em qualquer lugar alcançável, em que c1 e c2 calhem de valer juntos; não é preciso ciclo nem raciocínio infinito, um único estado ruim basta como contraexemplo completo, exatamente de acordo com o padrão de violação de segurança da seção de Teoria Central.

Requisição e resposta

Sejam req e ack proposições atômicas para "uma requisição ocorreu" e "uma confirmação ocorreu". A propriedade □ (req → ◇ ack) diz: sempre, se uma requisição ocorre, então uma confirmação acaba ocorrendo depois; uma propriedade de vivacidade paradigmática, já que exige que algo bom (ack) acabe acontecendo em resposta a outra coisa, sem limite de quanto tempo esse "acabar" pode levar. Como é uma afirmação de vivacidade, seu contraexemplo é exatamente a estrutura de laço recém-apresentada: um prefixo finito que chega a um estado em que req se tornou verdadeiro, seguido de um ciclo de estados em que o caminho dá voltas para sempre sem que ack ocorra em nenhum ponto desse ciclo. Concretamente, imagine um prefixo Idle → Requested, seguido de um ciclo de dois estados Requested → Waiting → Requested → Waiting → ... que se repete indefinidamente, com ack nunca rotulado como verdadeiro em Requested nem em Waiting. Esse laço é uma representação completa e finita do caminho infinito ruim "a requisição acontece, depois o sistema fica dando voltas para sempre em um ciclo Requested/Waiting, sem nunca confirmar"; exatamente o tipo de rastro que um model checker como o SPIN relataria quando essa propriedade falha, dando a um engenheiro algo concreto e finito para inspecionar, embora a violação subjacente seja fundamentalmente um fato sobre comportamento infinito.

Até (until)

A propriedade ¬grant 𝖴 ready diz: grant está ausente enquanto ready ainda não se tornou verdadeiro e (esta é a parte exigente da semântica de 𝖴) ready precisa de fato acabar se tornando verdadeiro. Não basta grant simplesmente ficar ausente para sempre enquanto ready também nunca ocorre; se ready nunca acontecer em nenhum ponto do caminho, a fórmula de until é falsa, não importa o que grant faça, porque a semântica do operador exige explicitamente que seu lado direito acabe valendo. É precisamente a sutileza apontada como equívoco comum abaixo: 𝖴 é um compromisso estritamente mais forte do que uma leitura informal de "até" como na linguagem comum poderia sugerir, e tratá-lo como equivalente a uma fórmula mais fraca do tipo "P vale até quando, se algum dia, Q ocorrer" (um operador LTL genuinamente diferente, às vezes chamado de weak-until) muda silenciosamente o que está de fato sendo afirmado.

• Usar ◇ quando na verdade é preciso □, transformando um invariante pretendido em uma eventualidade única. ◇ safe só exige que o sistema esteja seguro em algum ponto, possivelmente de forma breve e possivelmente só uma vez antes de ficar inseguro para sempre; essa é uma afirmação dramaticamente mais fraca que □ safe, que quem escreveu a propriedade quase sempre quis dizer de fato, e confundir as duas transforma silenciosamente uma propriedade de "sempre" pretendida em uma propriedade de "às vezes" acidental.
• Esquecer que a LTL fala de um caminho por vez. A verdade de toda fórmula LTL é definida em relação a um único caminho fixo; afirmações sobre "todas as execuções possíveis" exigem checar a fórmula contra todo caminho que o modelo admite, um de cada vez (ou por um algoritmo que efetivamente faça isso), e não contra alguma execução representativa escolhida arbitrariamente.
• Presumir que falhas de vivacidade sempre têm contraexemplos finitos curtos e fáceis de encontrar. Como a discussão sobre laços deixa explícito, uma violação de vivacidade é fundamentalmente uma afirmação sobre comportamento infinito, e sua testemunha mínima (prefixo mais ciclo) pode exigir explorar uma parte substancialmente maior do espaço de estados do que uma violação de segurança comparável exigiria; é parte do motivo de a checagem de vivacidade ser algoritmicamente mais exigente que a checagem de segurança, uma distinção a que model-checking-exhaustive-state-space-exploration volta diretamente.
• Escrever premissas de justiça como comentários ou notas informais em vez de premissas formais dentro do modelo ou da propriedade. Muitas propriedades de vivacidade só são verdadeiras sob uma premissa de justiça (fairness), por exemplo "se um processo tenta repetidamente entrar na sua seção crítica, ele acaba sendo escalonado", e, se essa premissa for deixada sem enunciado formal, um model checker vai (corretamente, dado o que de fato lhe foi pedido) encontrar um contraexemplo em laço construído inteiramente de escalonamento injusto, um que nunca ocorreria sob nenhum escalonador justo no sistema real; a correção é codificar a premissa de justiça explicitamente, e não desconfiar do contraexemplo.

A Lógica Temporal Linear dá aos requisitos de segurança e de vivacidade ("nada de ruim nunca acontece" e "algo bom acaba acontecendo") uma forma matemática precisa, usando os operadores □, ◇, ○ e 𝖴 para descrever propriedades de um único caminho de execução infinito, e não de um único estado final. Violações de segurança são testemunhadas por um prefixo ruim finito, enquanto violações de vivacidade exigem a noção genuinamente diferente de um laço (um prefixo finito que leva a um ciclo que evita o evento prometido para sempre), representando um caminho infinito ruim que nenhum rastro finito sozinho conseguiria representar diretamente. ctl-and-branching-time-logic continua a seguir perguntando o que muda quando o futuro de um sistema não é um único caminho, mas uma árvore ramificada de possibilidades; uma distinção que importa muito quando o não determinismo representa escalonamento ou escolhas do ambiente genuínas, e não algo que um único caminho fixo consiga capturar.