logic - 构建有效的 CTL 或 LTL 表达式(在 NuSMV 中)

Question

我正在尝试创建有效的 CTL 或 LTL 表达式以在 NuSMV 中进行模型检查。

我在游戏中有一个变量， Actor 们四处奔跑试图捕获对方。 变量是 State_Of_Game :{Win,Lose,Playing}

我想表达的是，从每个开始状态来看，游戏都可能赢或输。

那么，我如何在 CTL 或 LTL 中实现这一点？

我正在考虑类似 AG (S_O_G = Win | S_O_G = Lose) 的东西，但不知道如何实现从每个起始状态都可以看到它。

Answer 1

我不熟悉SMV表示法，所以我对此进行猜测，但关键点是:

1. 为了避免量化外部的所有状态:您不想说所有游戏都可以赢或输，而只能说开始的游戏。因此，只需在起始状态有一个公式，没有最外层模态

2. 要使用合取而不是析取:您想要断言可赢性和可输性

3. 您需要单独的模式来包装每个分支:获胜性、失败性是一种存在主义主张，表示有可能达到某个条件。

我认为您需要的公式是:根处的 (EG SOG=Win) & (EG SOG=Lose) ，这可能意味着类似于 init/start 子句，或在命名根子句处断言。如果 SMV 没有 EG 模态，则可以使用等价 EG p = !(AG !p) 将其转换为 AG，因为两者是 De Morgan 对偶。