This plugin allows one to check the compliance of a process model expressed as a Petri net, against a set of business rules expressed in CTL (Computation Tree Logic). To use this plugin, select a PNML model and click on “Analyze>Check compliance against CTL rules”. A dialog window pops up asking to import an XML file or input a CTL specification which captures the business rules to be checked. This CTL specification may be obtained from a set of process models via the Extract CTL rules from process model(s) plugin.
The plugin returns an overview of all CTL rules in the specifications, marked green when they are complied with by the model (the rule evaluates to true), or marked red when they are not complied with (the rule evaluates to false).
A screencast of this plugin is available here.