Lógica de Árvore de Computação

Lógica de Árvore de Computação (LAC) é uma ramificação-temporal da Lógica, significando que seu modelo de tempo é como a estrutura árvore no qual o futuro não é determinado. Não tem caminhos diferentes no futuro, qualquer um deles pode ser um caminho atual que é realizado. É usado na verificação formal de artefatos de software ou hardware, tipicamente por aplicações de software conhecidas como verificadores de modelos que determina se um dado artefato possui propriedades de segurança ou liveness. Por exemplo, LAC pode especificar que quando alguma condição inicial é satisfeita (ex: todas as variáveis do programa são positivas ou não há carros na estrada que escarrancham duas pistas ), então todas as possíveis execuções do programa evitam alguma condição indesejável (ex: dividir um número por zero ou o a colisão de dois carros na estrada) . Neste exemplo, a propriedade de segurança pode ser verificada por um modelo verificador que explora todas as possibilidades de transações para fora de um programa de estados satisfazendo a condição inicial que garante que todos as execuções satisfazem esta propriedade. Lógica de Árvore de Computação está na classe de Lógica temporal que inclui Lógica Temporal (LLT). Embora aqui existam propriedades expressáveis em apenas uma das LAC ou LLT, todas as propriedades em ambas as lógicas podem ser expressas em .