我很难理解我们如何使用线性时间逻辑对这些自动机建模。有人可以请在此链接图片中的案例上向我解释这一点，或者将我指向一个在示例中解释这一点的来源。
我提前感谢您的帮助。
问问题
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 回答