Como provar que uma fórmula não pode ser expressa em LTL, mas pode estar nos autômatos Buchi?

Estou procurando uma técnica geral que possa me ajudar a provar não apenas que os autômatos Buchi são um modelo mais expressivo que o LTL, mas que a fórmula específica pode / não pode ser expressa em LTL.

Por exemplo, " ocorre pelo menos em posições pares" pode ser descrito pelos seguintes autômatos Buchi: que e . $p$ $({q_0, q_1}, \Sigma, \delta, q_0, \{q_0\})$ $\delta(q_1, *) = q_0$ $\delta(q_0, p) = q_1$

Eu li que esse autômato não pode ser expresso em LTL, mas não entendo como prová-lo formalmente.

Obrigado.

lo.logic automata-theory Daniil
fonte

Engraçado. Eu estava olhando para os slides hoje também.

587 Dave Clarke

Respostas:

Primeiro, você precisa saber o que deseja expressar e como vai expressá-lo. Por exemplo, você pode representar uma propriedade como um conjunto de rastreios infinitos.

$\omega$ $\omega$

A Seção 5.1 de Princípios de verificação de modelo por Baier e Katoen é um bom ponto de partida elementar. Se você deseja técnicas de prova gerais, existem várias maneiras de proceder. Uma técnica geral que me agrada é usar jogos. O primeiro jogador está tentando mostrar que duas estruturas podem ser distinguidas com uma fórmula LTL. O segundo mostra que eles são os mesmos. Duas estruturas são equivalentes a LTL se o segundo jogador tiver uma estratégia vencedora. Portanto, se você usar duas estruturas que não são isomórficas, mas o segundo jogador tiver uma estratégia vencedora, não haverá uma fórmula LTL para distinguir as duas.

Hierarquia Até e Outras Aplicações de um Jogo de Ehrenfeucht-Fraisse para Lógica Temporal , K. Etessami e Th. Wilke.

$\omega$

Definibilidade lógica em traços infinitos , Werner Ebinger e Anca Muscholl

Vou cavar um pouco mais e tentar encontrar uma apresentação mais algorítmica.

Vijay D
fonte

ω

$\omega$

Portanto, se eu provar que uma propriedade específica pode ser expressa apenas em linguagem regular sem estrela, segue-se que a propriedade não pode ser expressa em LTL. Então, eu estou procurando uma técnica para provar isso para propriedades específicas.

Daniil

ω

$\omega$

ω

$\omega$

Eu, pessoalmente, prefiro técnicas algébricas. Minha intuição é terrível em geral e descobri que as técnicas algébricas me levam a menos arenques vermelhos e provas mais curtas. No entanto, a partir de rejeições e apresentações em papel, tenho a impressão de que a maioria dos cientistas da computação prefere jogos ou técnicas de prova relacional (bisimulação, etc.).

precisa

Eu sugeriria o uso da caracterização de linguagens de primeira ordem por autômatos Büchi livres de contra-ataque: veja, por exemplo, V. Diekert e P. Gastin, linguagens definíveis de primeira ordem . Em Lógica e Automata: História e Perspectivas, Textos em Lógica e Jogos 2, páginas 261--306. Amsterdam University Press, 2008. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DG-WT08.pdf

PS: em palavras finitas, esta coluna BEATCS também é muito útil: J.-E. Pin, Logic on Words , http://hal.archives-ouvertes.fr/hal-00020073 .

Sylvain
fonte

$\omega$

$\omega$ $x\in S$ $n$ $x^n=x^{n+1}$

Isso fornece um algoritmo para definição de LTL.

Denis
fonte