有没有一个Python包可以对有限状态机进行时态逻辑模型检查？

Question

我希望能够将系统建模为有限状态机，并根据时序逻辑规范测试模型的属性。在

我知道StateFlow的模型检查功能，但如果可能的话，我更喜欢使用Python，因为它是开源的。我也知道郁金香是设计和模拟有限状态机的可靠选择，但据我所知，它不做模型检查。pythonwiki上的FSM包列表似乎充满了类似的以实现为中心的包。在

有人知道一个不同的Python包，它能够根据时序逻辑设计规范进行模型检查吗？在

Answer 1

有很多免费的模型检查工具，比如NuSMV和Spinhttps://en.wikipedia.org/wiki/List_of_model_checking_tools

https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md

我怀疑您是否找到了许多基于python的工具，但是有一些是可用的

PyNuSMV-NuSMV的python前端，无工业强度模型检查器https://github.com/sbusard/pynusmv

Spot-一个用于使用python绑定进行模型检查的LTL omega自动机库https://spot.lrde.epita.fr/

小型CTL，CTL*和LTL Buchi自动机模型检查器https://github.com/albertocasagrande/pyModelChecking

PyBoolNet是NuSMV https://github.com/hklarner/PyBoolNet的前端以及其他布尔网

无畏https://github.com/formalmethods/intrepyd

硬件LTL模型检查器https://github.com/cristian-mattarei/CoSA

HyLaa混合系统模型检验器https://github.com/stanleybak/hylaa