Skip to main content

A package for Timed CTL model checking in Python

Project description

pyTCTL

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

This version

0.1

Download files

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

Files for pyTCTL, version 0.1
Filename, size File type Python version Upload date Hashes
Filename, size pyTCTL-0.1-py3-none-any.whl (2.4 kB) File type Wheel Python version py3 Upload date Hashes View hashes
Filename, size pyTCTL-0.1.tar.gz (2.1 kB) File type Source Python version None Upload date Hashes View hashes

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page