CauseJMu is a multi-threaded application that automatically computes causalities with respect to Hennessy Milner Logic (HML) reachability properties, within a Labelled Transition System (LTS) model. CauseJMu relies on the interplay between the mCRL2 toolset and Java. The former exploits the model-checking capabilities of mCRL2, whereas the latter automatically devises mCRL2-compatible specifications based on a user-defined LTS and HML property.

The tool can be downloaded as a Java jar file under the below link.

[Download Tool