python - 是否有可以对有限状态机进行时间逻辑模型检查的 Python 包？

Question

已结束。此问题不符合 Stack Overflow guidelines .它目前不接受答案。

---

我们不允许提出有关书籍、工具、软件库等方面的建议的问题。您可以编辑问题，以便用事实和引用来回答它。

关闭3年前。

Improve this question

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

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

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

Answer 1

有很多免费的模型检查器，例如 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 绑定(bind)进行模型检查 https://spot.lrde.epita.fr/

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

PyBoolNet NuSMV 的前端 https://github.com/hklarner/PyBoolNet连同 misc bool net

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

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

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