Charlie

Charlie -- an extensible Petri net analysis tool. Charlie is an extensible thread-based Java tool for analysing Petri nets. Its built-in functionalities apply standard analysis techniques of Petri net theory (e.g. invariants, siphon/trap property) to determine structural and behavioural properties of place/transition Petri nets, complemented by explicit CTL and LTL model checking. Charlie comes with a plugin mechanism, which permits to easily extend its basic functionality as it has been demonstrated for, e.g., structural reduction and time-dependent Petri nets. Charlie’s primary focus is teaching. For thispurpose, it has a rule system comprising standard theorems of Petri net theory to possibly decide further properties based on the already determined ones. All applied rules are reported by default, so the user may keep track of all analysis steps. The tool is in use for model verification of technical systems, especially software-based systems, as well as for model validation of natural systems, i.e. biochemical networks, such as metabolic, signal transduction, and gene regulatory networks. It is publicly available at url{http://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Charlie}.