Abstract
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üchi 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 calculus model checker of LTSmin for proper CTL* formulae (using a translator from CTL* to -calculus available in LTSmin). As far as we know, RGMEDD* is the only available Büchi-based CTL* model checker.
Cite
CITATION STYLE
Amparore, E. G., Donatelli, S., & Gallà, F. (2020). A CTL* Model Checker for Petri Nets. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12152 LNCS, pp. 403–413). Springer. https://doi.org/10.1007/978-3-030-51831-8_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
