A package for Timed CTL model checking in Python
A package for TCTL model checking in Python
The initial implementation makes use of NetworkX's DiGraph for the representation of Kripke structures.
The provided algorithms implement Lepri et al.'s approach to continuous TCTL model checking. Thus, this package also implements pointwise TCTL model checking.
The code was originally developed for the CREST project, but it seems better to extract the code into its own library.
@albertocasagrande is working on a similar library for (untimed) CTL/LTL/CTL* model checking called pyModelChecking.
His approach shares some of the ideas of this project. However, it seems that he chooses to implement Kripke structures directly (no networking library) and adds some features that I probably won't implement (e.g. a text parser). On the other hand, as far as I can see there's only one algorithm hardcoded for each temporal logic. In comparison, I plan to add the possibility to add and choose between search heuristics.
I will keep following his project. Maybe we can merge forces once I know more clearly which path the pyTCTL project is going to take.
Release history Release notifications | RSS feed
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.