使用SPIN进行LTL模型检查

我正在查看SPIN软件。我想用它来找到LTL理论的模型。所有的手册和教程讨论验证算法的属性，但我根本不感兴趣。我只想找到LTL公式的模型（我猜想是相应的Büchi自动机），就像mace4或paradox模型检测器可以找到FOL公式的模型。我相信SPIN应该能够做到这一点，但我无法在文档中找到它。有人能指出任何有用的资源吗？使用SPIN进行LTL模型检查

来源

2017-08-02 user1747134

我不知道我理解你的问题。但是如果你想从一个ltl公式生成一个Buchi自动机，你可以使用[this]（http://www.lsv.fr/~gastin/ltl2ba/index.php） –

谢谢，这正是我期待的对于。 – user1747134

这[问题/答案]（https://stackoverflow.com/questions/38780330/how-to-transform-ltl-into-automato-in-promela-spin）可能与您的需求有些相关。 –

为了从LTL公式中生成Buchi自动机，您可以使用ltl2ba工具。该工具可以提供Büchi自动的图形表示或它的一个PROMELA代码版本，如在下面的例子：

~$ ./ltl2ba -f "([] q0) && (<> ! q0)" 
never { /* ([] q0) && (<> ! q0) */ 
T0_init: 
    false; 
}

也可以使用自旋以产生PROMELA版本Büchi自动的，用命令：

~$ spin -f "LTL_FORMULA"

例如为：

~$ spin -f "[] (q1 -> ! q0)" 
never { /* [] (q1 -> ! q0) */ 
accept_init: 
T0_init: 
    do 
    :: (((! ((q0))) || (! ((q1))))) -> goto T0_init 
    od; 
}

然而，在具有ltl2ba，自旋对比度似乎并不生成的源代码时，使得有时难以解释它的输出，以简化Büchi自动; 例如尝试运行spin -f "([] q0) && (<> ! q0)"并将输出自动机与使用ltl2ba获得的输出自动机进行比较。

编辑

现在，您可以使用gltl2ba在sostitution为ltl2ba的网站，例如：

~$ gltl2ba.py -f "([] p0) || (<> p1)" -g 

never { /* ([] p0) || (<> p1) */ 
T0_init: 
    if 
    :: (1) -> goto T0_S1 
    :: (p1) -> goto accept_all 
    :: (p0) -> goto accept_S2 
    fi; 
T0_S1: 
    if 
    :: (1) -> goto T0_S1 
    :: (p1) -> goto accept_all 
    fi; 
accept_S2: 
    if 
    :: (p0) -> goto accept_S2 
    fi; 
accept_all: 
    skip 
}

生成以下图表：

来源

2017-08-02 12:16:40

谢谢。在线工具中是否有一种简单的方法将输出转换为DOT/PNG图形？可以将'ltl2ba -d'的输出以某种方式更改为DOT？ – user1747134

@ user1747134在我看来，最简单也是最可靠的方法就是为所生成的* Promela *代码编写一个简单的解析器/脚本。用'-d'获得的输出似乎并不完整，例如它没有明确说明* init *状态是否接受。 –

使用SPIN进行LTL模型检查

回答

相关问题