将状态转换系统转换为属性LTL公式
在有界模型检测的上下文中，人们将系统描述为一个状态转换系统以及需要检查的属性。
当需要向Model Checker工具提供多个系统描述和属性时，手动编写属性可能会变得单调乏味。在我的例子中，我使用LTL (线性时态逻辑)和一阶逻辑相结合。如何自动化翻译/解析系统描述并从中导出可验证属性的过程(理想情况下，一组初始状态、一组转换、一组状态)。例如，考虑给定here的微波示例
有了这样的系统描述，我如何才能以一种有效的方式达到规范？据我所知，没有这样的开源工具可以做到这一点。欢迎任何在思想和理论方面的方法。
回答 2
Stack Overflow用户
发布于 2018-02-26 00:46:49
您不能像您建议的那样从自动机自动派生LTL公式，因为自动机比LTL公式更具表现力。
这给您留下了两个主要的选择: 1.找到一个验证工具，它可以接受直接表示为自动机的规范(我不确定哪些是这样做的，但我怀疑这个特性值得检查SPIN和NuSMV )，或者2.使用一种元规范语言来简化规范的编写；例如，https://www.isp.uni-luebeck.de/salt (doi: 10.1007/10.1007_41)或IEE1850/PSL。虽然PSL更多地是工具实现者的语言定义，但SALT已经提供了一个web前端，可以将您的输入直接转换为LTL。
(顺便说一句，我发现你的方法在方法论上很有挑战性:你不应该从你的模型中推导公式，而是从你的初始系统描述中推导出公式，因为你要验证的正是这个模型。但是，如果我正确理解了您问题中的这一点，我不能百分之百确定。)
Stack Overflow用户
发布于 2018-05-02 03:06:24
我认为一个系统的属性，例如微波系统，来自技术和常识的期望和需求，而不是模型。微波炉应该是用来烹调食物的。但是它不应该在门打开的情况下做饭。然而，典型LTL模式的存储库对于定义属性很有用。它还列出了属性以及更熟悉的regex和自动机属性。
如果您确定仍要将自动机转换为LTL，请自动检查https://mathoverflow.net/questions/96963/translate-a-buchi-automaton-to-ltl
堪萨斯规范属性存储库http://patterns.projects.cs.ksu.edu/documentation/patterns.shtml
https://stackoverflow.com/questions/48863219
复制相似问题
腾讯云开发者
