PV3 McRERSchecks interruptible LTL property for a labelled transition system

Application domain/field

Type of tool

Model checker

Expected input


Expected output

Text file with the results. It will contain a summary of the results at the end which indicates how many results were right, wrong or unknown (and the time taken).


The tool seems to have a 'property analyzer' which can be used to determine whether a property is interruptible. This model checker is meant to be used for checking interruptible properties. This tool uses the same semantics for LTSs, LTL, and satisfiability as the RERS (verification competition/challenge). It uses the Spot library to determine equivalence of LTL formulas, determine language equivalence of BAs (Büchi automata), and to convert LTL formula to BA.
LTL Model checking


Artifact (CAV 2020): https://vsl.cis.udel.edu/cav2020/

Related papers

Action-Based Model Checking: Logic, Automata, and Reduction

Last publication date

14 July 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.