CTL e Lógica de Tempo Ramificado

• Explicar o que significa uma lógica temporal ser de tempo ramificado, em vez de tempo linear, e por que a distinção importa para sistemas não determinísticos.
• Usar os quantificadores de caminho A ("todos os caminhos") e E ("existe um caminho") junto com operadores temporais para enunciar fórmulas CTL com precisão.
• Distinguir AG, EF, AF e EG e dar um requisito concreto que cada um expressa naturalmente.
• Explicar por que fórmulas CTL são avaliadas em estados, e não ao longo de rastros inteiros, e o que isso significa para o modo como uma violação é relatada.
• Reconhecer quais requisitos do dia a dia têm formato natural de LTL e quais têm formato natural de CTL, e explicar por que nenhuma das lógicas simplesmente engloba a outra.

linear-temporal-logic-ltl se comprometeu com um único formato fixo de pergunta: dado um caminho linear por uma estrutura de Kripke, uma fórmula vale ao longo dele? Esse compromisso está exatamente certo para muitas propriedades, mas ele presume silenciosamente que não existe algo que sistemas reais muitas vezes têm: a partir de um estado, pode haver muitos futuros possíveis diferentes, ramificando conforme a escolha não determinística que um escalonador, um ambiente ou um componente subespecificado calhar de fazer em seguida. A LTL, avaliada caminho por caminho, ainda consegue expressar fatos sobre "todo caminho possível" exigindo que uma fórmula valha em todos eles, mas não tem como dizer, dentro de uma única fórmula, "existe algum futuro em que isto acontece" de forma distinta de "isto acontece em todo futuro"; as duas coisas acabam exigindo raciocínio separado sobre todo o espaço de caminhos, de fora da própria lógica.

A CTL (Computation Tree Logic, lógica de árvore de computação) é construída para tornar exatamente essa distinção uma parte de primeira classe da própria sintaxe da fórmula, quantificando explicitamente sobre caminhos em cada ponto em que um operador temporal é usado. A estrutura ramificada das continuações possíveis a partir de um dado estado não é algo sobre o que a CTL raciocina indiretamente depois; ela está embutida diretamente no significado de toda fórmula. Isso acaba importando muito em sistemas em que o não determinismo representa genuinamente possibilidades reais alternativas, e não um artefato da abstração (um escalonador que pode executar qualquer um de vários processos prontos em seguida, um protocolo cujo ambiente pode enviar qualquer uma de várias mensagens possíveis), porque "o sistema pode se recuperar" e "o sistema sempre acaba se recuperando, não importa o que o escalonador ou o ambiente façam" são garantias muito diferentes, e a CTL é construída para deixar uma fórmula dizer com precisão qual delas está sendo afirmada.

Quantificadores de caminho

A CTL prefixa cada operador temporal com um de dois quantificadores de caminho, e nenhum operador temporal é usado sozinho, ao contrário da LTL. A significa "para todos os caminhos a partir do estado atual": a afirmação precisa valer não importa qual dos possivelmente muitos futuros de fato se desenrole. E significa "existe pelo menos um caminho a partir do estado atual": a afirmação só precisa valer ao longo de algum futuro, sem nenhum compromisso sobre os outros. Esses dois quantificadores são o que permite à CTL distinguir, de forma sintática e sem ambiguidade, uma garantia que vale universalmente em toda continuação possível de uma mera possibilidade que vale ao longo de pelo menos uma.

Formas comuns

Quatro combinações de um quantificador de caminho com um operador temporal cobrem a grande maioria das propriedades de que esta disciplina precisa da CTL. AG P ("em todos os caminhos, P vale globalmente, sempre") é o análogo direto em CTL do □ P da LTL, mas fortalecido pelo quantificador de caminho universal explícito: P precisa valer em todo estado alcançável ao longo de todo futuro possível, e não só ao longo de um caminho específico escolhido para checar. EF P ("existe um caminho ao longo do qual P acaba valendo") é uma afirmação de pura possibilidade: diz que um estado que satisfaz P é alcançável por alguma sequência de escolhas, sem afirmar nada sobre o que acontece se outra sequência de escolhas for feita. AF P ("em todos os caminhos, P acaba valendo") é consideravelmente mais forte que EF P: exige que todo futuro possível, não importa quais escolhas sejam feitas pelo caminho, acabe chegando a um estado que satisfaz P, excluindo até uma única sequência ruim e azarada de escolhas que consiga evitar P para sempre. EG P ("existe um caminho ao longo do qual P vale globalmente") diz que pelo menos um futuro possível mantém P verdadeiro para sempre, sem afirmar nada sobre se outros futuros diferentes podem acabar saindo de P.

Fórmulas de estado

Uma característica estrutural definidora da CTL, que vale enunciar explicitamente porque difere da convenção da LTL: fórmulas CTL são avaliadas em estados individuais, e não ao longo de rastros inteiros. Perguntar "AG P vale?" é, na verdade, perguntar "P vale neste estado, e em todo estado alcançável a partir dele ao longo de todo caminho possível?"; a árvore ramificada de toda continuação possível a partir daquele estado é dobrada diretamente no significado da fórmula naquele estado, em vez de a fórmula receber um caminho específico para checar, como acontece com uma fórmula LTL. Essa avaliação centrada em estados é exatamente o que torna a CTL um encaixe natural para consultas com sabor de alcançabilidade ("o sistema consegue chegar a um estado recuperado a partir daqui?" ou "o sistema precisa acabar chegando a um estado recuperado a partir daqui, não importa o quê?"), enunciadas diretamente como uma propriedade do estado atual, sem exigir antes um raciocínio separado sobre um caminho inteiro.

LTL versus CTL

Nenhuma das lógicas é simplesmente um caso especial ou um superconjunto estrito da outra, e reconhecer qual formato um dado requisito de fato tem é a habilidade prática que este conceito constrói. A LTL consegue expressar com real elegância muitas propriedades lineares de justiça (fairness) e de resposta; um requisito enunciado naturalmente como uma afirmação sobre a sequência de eventos que se desenrola ao longo de uma execução (como "se este evento se repete infinitas vezes, aquele outro evento também precisa se repetir infinitas vezes") tende a se traduzir de forma limpa em LTL e pode resistir completamente a uma tradução limpa em CTL. A CTL, por outro lado, consegue distinguir "possível" de "inevitável" diretamente na sintaxe de uma única fórmula (EF recovered versus AF recovered), uma distinção que não tem nenhuma fórmula LTL equivalente, porque fórmulas LTL são checadas caminho por caminho e não têm um jeito nativo de quantificar sobre o conjunto de caminhos de dentro da própria fórmula. Escolher a lógica certa para um dado requisito, em vez de forçar toda propriedade na lógica que calhar de ser mais familiar, é parte de fazer bem a especificação formal.

Recuperação possível

A propriedade EF recovered diz: a partir do estado atual, existe pelo menos um caminho ao longo do qual o sistema acaba chegando a um estado rotulado recovered. É uma afirmação de pura possibilidade, e deve ser lida exatamente assim e nada mais: estabelecer EF recovered prova que a recuperação é alcançável sob alguma sequência de escolhas, mas não diz absolutamente nada sobre se um escalonador real azarado ou um ambiente adversarial poderia, em vez disso, conduzir o sistema por outro caminho que nunca chega à recuperação. Confundir uma prova de EF recovered com uma garantia de que o sistema "vai" se recuperar é exatamente a lacuna que este operador foi construído para expor, e não para esconder.

Reset inevitável

A propriedade AF reset diz: em todo caminho possível a partir do estado atual, reset acaba acontecendo, não importa qual sequência de escolhas não determinísticas de fato seja feita. É uma afirmação substancialmente mais forte que a mera alcançabilidade: provar AF reset exclui até um único caminho infinito que consiga evitar reset para sempre, por mais artificial ou improvável que essa sequência específica de escolhas pareça. Um único caminho infinito que nunca chega a um estado rotulado reset, encontrado em qualquer ponto da árvore ramificada de futuros possíveis, é uma refutação completa de AF reset, exatamente porque o quantificador "para todos os caminhos" não é satisfeito se até um caminho for um contraexemplo; isso é bem mais forte que "reset é alcançável" (EF reset), que esse mesmo caminho teimoso não refutaria de jeito nenhum.

Segurança global

A propriedade AG ¬error diz: em todo caminho a partir do estado atual, e em cada ponto ao longo de cada um desses caminhos, error é falso. Para um sistema de transição finito, isso se reduz a uma pergunta que, na prática, é computacionalmente mais simples do que parece à primeira vista: algum estado rotulado error é alcançável a partir do estado atual, seguindo qualquer caminho de transições? Se nenhum estado rotulado error for alcançável por nenhuma sequência de transições, então trivialmente nenhum caminho consegue chegar a um, e AG ¬error vale; se algum estado rotulado error for alcançável por pelo menos uma sequência de transições, esse único estado alcançável (rastreado de volta até um caminho concreto a partir do estado inicial) é um contraexemplo completo de AG ¬error, não importa quantos outros caminhos o evitem com sucesso. Essa redução de uma propriedade de segurança universalmente quantificada sobre caminhos a uma simples pergunta de alcançabilidade é exatamente o motivo de a checagem de segurança no estilo AG, ao contrário da checagem de vivacidade com AF ou EG, não exigir raciocínio sobre ciclos ou comportamento infinito: um único estado ruim alcançável, encontrado em qualquer lugar, já resolve a questão.

• Confundir EF com AF. EF P só exige que algum caminho acabe chegando a P; AF P exige que todo caminho chegue. Como o exemplo do reset inevitável mostra diretamente, um único caminho infinito que evita P para sempre refuta AF P e deixa EF P totalmente intocado; são forças de garantia genuinamente diferentes, e não variantes estilísticas da mesma afirmação.
• Achar que "existe um caminho bom" (EF, EG) basta para constituir uma garantia real. EF recovered só estabelece que a recuperação é possível sob alguma sequência favorável de escolhas; não diz nada sobre o que acontece sob uma desfavorável, e tratar uma propriedade quantificada com E como se fosse a garantia mais forte quantificada com A é o caminho direto para afirmar mais do que foi provado.
• Esquecer que fórmulas CTL são avaliadas em estados, e não ao longo de rastros inteiros. Ao contrário de uma fórmula LTL, que é checada contra um caminho específico que lhe é entregue, a verdade de uma fórmula CTL em um estado já codifica uma afirmação sobre toda a árvore ramificada de futuros alcançáveis a partir daquele estado; não há um passo separado de "escolher um caminho primeiro e depois checar a fórmula", como existe implicitamente na LTL.
• Presumir que toda fórmula LTL tem uma fórmula CTL equivalente e simples (ou vice-versa). Como a seção de Teoria Central diz diretamente, as duas lógicas não estão aninhadas uma na outra: algumas propriedades LTL, especialmente as construídas em torno de justiça ao longo de uma única execução inteira, não têm nenhuma fórmula CTL equivalente, e vice-versa para algumas propriedades que quantificam explicitamente sobre a estrutura ramificada dos futuros possíveis; escolher a lógica errada para um requisito pode tornar uma propriedade que seria natural desajeitada ou até impossível de enunciar.

A CTL traz a estrutura ramificada dos futuros possíveis diretamente para a sintaxe da própria fórmula, combinando cada operador temporal com um quantificador de caminho explícito (A para todo futuro possível, E para algum futuro possível), o que permite distinguir, dentro de uma fórmula, garantias que valem não importa o que um escalonador ou ambiente faça de meras possibilidades que valem ao longo de pelo menos uma sequência favorável de escolhas; uma distinção para a qual a avaliação caminho a caminho da LTL não tem sintaxe direta. O AG reduz a checagem de segurança à simples alcançabilidade, enquanto AF e EG exigem raciocinar sobre se todo (ou algum) futuro possível acaba chegando a (ou evita para sempre) uma condição-alvo; um raciocínio que, como model-checking-exhaustive-state-space-exploration desenvolve a seguir, exige um mecanismo algorítmico genuinamente diferente do de uma checagem de segurança. Nem a LTL nem a CTL simplesmente engloba a outra, e esta disciplina usa cada uma onde seu formato particular de quantificação de fato corresponde ao requisito sendo enunciado.