Qual é a diferença entre LTL e CTL?

Eu já li exemplos de fórmulas em CTL, mas não em LTL e vice-versa, mas estou tendo problemas para entender melhor as fórmulas de LTL e , na verdade , qual é a diferença.

Para realmente entender a diferença entre LTL e CTL, você deve estudar a semântica dos dois idiomas. As fórmulas LTL denotam propriedades que serão interpretadas em cada execução de um programa. Para cada execução possível (uma execução), que pode ser vista como uma sequência de eventos ou estados em uma linha - e é por isso que é chamado de "tempo linear" - a satisfação é verificada na execução, sem possibilidade de alternar para outra execução durante a verificação. Por outro lado, a semântica do CTL verifica uma fórmula em todas as execuções possíveis e tenta todas as execuções possíveis ( operador A ) ou apenas uma execução ( operador E ) ao enfrentar uma ramificação.

Na prática, isso significa que algumas fórmulas de cada idioma não podem ser declaradas no outro idioma. Por exemplo, a propriedade reset (uma importante propriedade de acessibilidade para o projeto de circuitos) afirma que sempre existe a possibilidade de que um estado possa ser alcançado durante uma execução, mesmo que nunca seja realmente alcançado ( redefinição AG EF ). O LTL pode apenas afirmar que o estado de redefinição foi realmente alcançado e não que pode ser alcançado.

Por outro lado, a fórmula LTL não podem ser traduzidos em CTL. Essa fórmula indica a propriedade da estabilidade: em cada execução do programa, s será finalmente verdadeiro até o final do programa (ou para sempre, se o programa nunca parar). Os CTL podem fornecer apenas uma fórmula muito rigorosa ( AF AGs ) ou muito permissiva ( AF EG s ). O segundo está claramente errado. Não é tão simples para o primeiro. Mas a AF AG s está errada. Considere um sistema que faça um loop na A1 , possa ir de A1 para B e depois vá para A2$\Diamond\Box s$no próximo passo. Então o sistema permanecerá no estado A2 para sempre. Então, "o sistema irá finalmente ficar em uma Um estado" é uma propriedade do tipo . É óbvio que essa propriedade se mantém no sistema. No entanto, os AG AG não podem capturar essa propriedade, pois o oposto é verdadeiro: existe uma execução na qual o sistema sempre estará no estado em que uma execução finalmente entra em um estado não A.$\Diamond\Box s$

Não sei se isso responde à sua pergunta, mas gostaria de adicionar alguns comentários.

Há muita discussão sobre a melhor lógica para expressar propriedades para verificação de software ... mas o verdadeiro debate está em outro lugar. O LTL pode expressar propriedades importantes para modelagem de sistema de software (justiça) quando o CTL deve ter uma nova semântica (uma nova relação de satisfação) para expressá-las. Mas os algoritmos CTL são geralmente mais eficientes e podem usar algoritmos baseados em BDD. Então ... não há melhor solução. Apenas duas abordagens diferentes, até agora.

Um dos comentaristas sugere o artigo de Vardi "Branching versus Linear Time: Final Showdown" .

Se determinado objeto (por exemplo, rastrear no caso de LTL), você considera apenas um futuro para cada ponto no tempo, em CTL você tem uma infinidade deles.

Em particular, nextfornece uma ação exclusiva no LTL, mas (potencialmente) um conjunto inteiro no CTL.