線形時相論理を使用してこれらのオートマトンをどのようにモデル化したかを理解するのに苦労しています。このリンクの写真にあるケースについて、誰かが私にこれを説明してください。または、例でこれを説明しているソースを教えてください。
よろしくお願いします。
質問する
185 次
1 に答える
0
LTL式はアルファベットで定義されています（これは通常「原子命題」と呼ばれ、例ではアルファベットは set です{x,y}）。LTL 式は、アルファベットのサブセットの無限シーケンスを、式を満たす (無限の) 単語と満たさない単語に分割します。たとえば、単語{x}, {x,y}, {}, {}...は式F not x and not yを満たしますが、式 を満たしませんGy。
Buchi オートマトンも同じことを行います。あるアルファベットで無限の単語を読み取り、その単語を受け入れるか拒否します。Vardi と Wolper は、与えられた LTL 式から、式を満たす無限の単語を正確に受け入れる Buchi オートマトンを構築できることを示しました。工事の様子はこちらでご覧いただけます。
于 2012-10-29T20:59:38.190 に答える