2

我正在尝试为 NuSMV 中的模型检查创建一个有效的 CTL 或 LTL 表达式。

我在游戏中有一个变量，演员四处奔跑试图互相抓住。变量是 State_Of_Game : {Win,Lose,Playing}

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

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

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

4

2 回答 2

3

我不熟悉 SMV 表示法，所以我在猜测，但关键点是：

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

  2. 使用连词，而不是析取：你想断言可赢性和可输性

  3. 您需要包装每个分支的单独形式：可赢性、可输性是一种存在性主张，即有可能达到某种条件。

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

于 2013-12-13T09:30:55.033 回答
-1

试试这个：AF(State_of_Game=Win| State_of_Game=Lose)

于 2019-05-30T23:57:38.323 回答