是否有一个Python包可以对有限状态机进行时态逻辑模型检查？
我希望能够将系统建模为有限状态机，并根据时序逻辑规范测试模型的属性。
我知道StateFlow的模型检查功能，但如果可能的话，我更愿意使用Python，因为它是开源的。我也知道TuLiP是设计和模拟有限状态机的可靠选择，但据我所知，它不进行模型检查。Python上的FSM包列表似乎充满了类似的面向实现的包。
有没有人知道一个不同的Python包，它能够根据时态逻辑设计规范进行模型检查？
回答 1
Stack Overflow用户
发布于 2019-04-05 15:01:51
有很多免费的模型检查程序，如NuSMV和Spin tools。
我怀疑您是否找到了许多基于python的工具，但是有一些是可用的。
PyNuSMV -一条蟒蛇前端趋向于NuSMV，工业强度无模型检查器https://github.com/sbusard/pynusmv
Spot -一个LTL-omega自动机库，用于使用python绑定https://spot.lrde.epita.fr/进行模型检查。
小CTL，CTL*和LTL Buchi自动机模型检查器https://github.com/albertocasagrande/pyModelChecking
PyBoolNet A前端NuSMV https://github.com/hklarner/PyBoolNet和misc bool网
Intrepyd https://github.com/formalmethods/intrepyd
硬件LTL模型检查器https://github.com/cristian-mattarei/CoSA
HyLaa混合系统模型检查器https://github.com/stanleybak/hylaa
https://stackoverflow.com/questions/55500256
复制相似问题
腾讯云开发者
