QCTL model-checking

qctlmc: a tool for QCTL model-checking

qctlmc is a prototype: it is under development !
It is developped by:

• Akash Hossain
• François Laroussinie

It is a Python3 program which builds a QBF formula (for a QBF solver) from a Kripke structure and a QCTL formula.
QCTLMC provides a QBF formula in QCIR format (for cqesto, qfm, qfun, ghostq) or in Z3 format. To use QCTLMC, you have to install at least one of these solvers !
The new version of QCTLMC uses PLY package: here.

How to get qctlmc ?

QCTLMC 2.2 (September, 2020): here.

• Version 2.1 (september 2020): here.
• Version 2.0 (february 2020) : here.
• Version 1.0 (only for Z3, June 2019): here.

Related papers:

About the reduction from QCTL to QBF:

• Akash Hossain, François Laroussinie. QCTL model-checking with QBF solvers. [ here ]
• Akash Hossain, François Laroussinie. From Quantified CTL to QBF. (Proc. of TIME 2019, 26th International Symposium on Temporal Representation and Reasoning, Malaga, Spain). [ here ]

About QCTL:

• François Laroussinie, Nicolas Markey. Quantified CTL: Expressiveness and Complexity. Logical Methods in Computer Science 10(4) , 2014. [ Abstract , PDF ]
• Amelie David, François Laroussinie and Nicolas Markey. On the expressiveness of QCTL. In Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016), [ Abstract , PDF ]

Email: francois.laroussinie[at]irif.fr