線性時序邏輯（LTL）NAD自動機建模

Question

我真的具有理解我們如何通過使用線性時序邏輯建模這些自動機的困難。請有人請向我解釋一下這個link圖片上的案例，或者向我指出一個可以解釋這個例子的來源。

我感謝你在你的幫助。

Answer 1

LTL公式在字母表定義（通常稱爲「原子命題」，並在實施例中的字母是集合{x,y}）。 LTL公式將字母表的子集的無限序列分割成滿足公式的（無限）字和不滿足的公式。例如，字{x}, {x,y}, {}, {}...滿足式F not x and not y，但不滿足式Gy。

布琪自動做同樣的。它讀取某個字母表上的無限單詞，並接受或拒絕該單詞。 Vardi和Wolper表明，根據LTL公式，有可能構造一個Buchi自動機，該自動機完全接受滿足公式的無限單詞。你可以看到建築here。