[SOLVED] Is there a Python package that can do temporal logic model-checking for finite state machines?

Is there a Python package that can do temporal logic model-checking for finite state machines?

I want to be able to model a system as a finite state machine and test the properties of the model against temporal logic specifications.

I am aware of StateFlow's model-checking capabilities, but if possible I would prefer to use Python because it is open-source. I am also aware of TuLiP as a solid option for designing and simulating finite state machines, but as far as I can tell it does not do model-checking. The FSM package list on the Python wiki seems to be full of similarly implementation-focused packages.

Does anyone know of a different Python package which is capable of model-checking per temporal logic design specifications?

Solution

There are plenty of free model checkers such as NuSMV and Spin https://en.wikipedia.org/wiki/List_of_model_checking_tools

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

I doubt that you find many python based tool, but there are a few available

PyNuSMV - a python frontend to NuSMV, industrial strength free model checker https://github.com/sbusard/pynusmv

Spot - an LTL-omega-automata library for model checking with a python binding https://spot.lrde.epita.fr/

Small CTL, CTL* and LTL Buchi automata model checker https://github.com/albertocasagrande/pyModelChecking

PyBoolNet A frontend to NuSMV https://github.com/hklarner/PyBoolNet along with miscellaneous utilities for analysing Boolean networks

Intrepyd a model checker and simulator within a python module, that allow rapid prototyping of "formal methods algorithms" https://github.com/formalmethods/intrepyd

pySMT-based hardware LTL model checker https://github.com/cristian-mattarei/CoSA

HyLaa Hybrid Systems model checker https://github.com/stanleybak/hylaa

Small CTL,CTL* and LTLmodel-checking package https://github.com/albertocasagrande/pyModelChecking