Qual é a implementação mais simples de todas as traduções decentes de LTL para Buchi ou outros algoritmos de verificação de LTL?

Estou escrevendo um verificador de modelo de brinquedo e estou no ponto em que é hora de implementar a tradução de autômato LTL para Buchi.

Por várias razões óbvias, desejo que o algoritmo seja simples :) por exemplo, quero que o código permaneça extremamente claro e conciso pelo maior tempo possível.

Analisei a abordagem "autômatos locais + autômatos de eventualidade", descrita em vários tutoriais, mas parece não ser simples de implementar / entender (a prova de correção é bastante grande), nem produz pequenos autômatos. Então, eu não vou implementá-lo até ter certeza de que não vou me arrepender :)

Então, eu ficaria grato por referências a artigos que descrevem algoritmos simples e eficientes para esta tradução, ou talvez simples e ineficientes - então artigos sobre minimização de autômatos Buchi também serão bem-vindos :)

... Ou talvez haja abordagens alternativas interessantes para a verificação LTL?

Para referência, veja uma genealogia dos algoritmos de tradução LTL para Buchi http://spot.lip6.fr/wiki/LtlTranslationAlgorithms . Alguém pode dizer algo sobre isso?

Uma construção não listada no site do SPOT é apresentada em uma pesquisa realizada por Demri & Gastin, Specification and Verification using Temporal Logics , 2009. A construção é simples e produz autômatos razoavelmente pequenos, para que possa ser executada manualmente para pequenas formulações, que é bom para o ensino (que é como eu o uso), mas também pode ser útil para depurar uma implementação. Eu não apostaria que fosse mais eficiente do que o usado pelo SPOT.

Sobre minimização, não há autômato Büchi mínimo canônico para uma determinada linguagem regular. Para obter autômatos menores, é possível quociente o autômato por alguma relação de simulação. Um artigo clássico sobre o assunto é de Etessami, Wilke & Schuller, Fair Simulation Relations, Parity Games e State Space Reduction para Büchi Automata , SIAM Journal on Computing 34: 1159-1175, 2005.$\omega$

Eu consideraria a tradução que passa por um autômato alternado. (Veja o artigo de Vardi "Autômatos alternados e verificação do programa"). É uma tradução muito elegante de LTL para autômatos alternados e, em seguida, você pode usar Mihano Ayashi (que também é elegante - é uma construção de subconjunto duplo) para alcançar um autômato Buchi não determinístico.