PV3 ⊧ McRERSchecks interruptible LTL property for a labelled transition system

Application domain/field

• Model checking
• Interruptible properties
• Stutter-invariant properties
• Partial order reduction
• Concurrent systems

Type of tool

Model checker

Expected input

• LTS (as a parallel composition)
• LTL formula to check

Format:

• LTS: Graphviz dot file
• LTL formula: text file

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

Internals

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.