Skip to main content

A package for Timed CTL model checking in Python

Project description


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.

Similar Projects

@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.

Project details

Release history Release notifications | RSS feed

This version


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

pyTCTL-0.1.tar.gz (2.1 kB view hashes)

Uploaded Source

Built Distribution

pyTCTL-0.1-py3-none-any.whl (2.4 kB view hashes)

Uploaded Python 3

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page