A CTL* Model Checker for Petri Nets

This tool paper describes RGMEDD*, a CTL* model checker that computes the set of states (sat-sets) of a Petri net that satisfy a CTL* formula. The tool can be used as a stand-alone program or from the GreatSPN graphical interface. The tool is based on the decision diagram library Meddly, it uses Spot to translate (sub)formulae into B <spacing diaeresis>uchi automata and a variation of the Emerson-Lei algorithm to compute the sat-sets. Correctness has been assessed based on the Model Checking Context 2018 results (for LTL and CTL queries), the sat-set computation of GreatSPN (for CTL) and LTSmin (for LTL), and the mu-calculus model checker of LTSmin for proper CTL* formulae (using a translator from CTL* to mu-calculus available in LTSmin). As far as we know, RGMEDD* is the only available Buchi-based CTL* model checker.