我希望能够将系统建模为有限状态机，并根据时间逻辑规范测试模型的属性。
我知道StateFlow的模型检查功能，但如果可能的话，我更喜欢使用Python，因为它是开源的。我也知道TuLiP是设计和模拟有限状态机的可靠选择，但据我所知，它不进行模型检查。Python wiki 上的 FSM 包列表似乎充满了类似的以实现为中心的包。
有谁知道不同的Python包能够根据时态逻辑设计规范进行模型检查？
有很多免费的模型检查器，如NuSMV和Spin https://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 - 一个LTL-omega-automata库，用于使用python绑定 https://spot.lrde.epita.fr/进行模型检查
小型 CTL、CTL* 和 LTL 布奇自动机模型检查器 https://github.com/albertocasagrande/pyModelChecking
PyBoolNet NuSMV https://github.com/hklarner/PyBoolNet 的前端以及杂项布尔网络
因特雷皮德 https://github.com/formalmethods/intrepyd
硬件零担模型检查器 https://github.com/cristian-mattarei/CoSA
HyLaa混合动力系统模型检查器 https://github.com/stanleybak/hylaa