ToolsUsed

The following software tools have been used and partly enhanced by the identified challenges while pursuing this project.


Snoopy


Design and animation/simulation of hierarchical graphs, among them (coloured) qualitative, stochastic, continuous and hybrid Petri nets.

Special features to support larger networks are

  • hierarchy (macro transitions, macro places),
  • logical nodes (transitions, places), and
  • colouring.

Snoopy reads and writes networks specified in SBML, Level 2, Version 3, and exports to about a dozen Petri net analysis tools, among them via the Abstract Petri Net Notation (APNN) and an extended version of it (APNN*). Additionally, simulation traces can be written as csv file.

Patty is a close friend of Snoopy and supports the animation of extended Petri nets within a web browser. Usability tips for web-based animation.

Snoopy website


Charlie


Analysis of qualitative (place/transition) Petri nets as well as the net structure of stochastic, continuous and hybrid Petri nets by the mathematical apparatus of Petri net theory, including

  • structural properties,
  • invariant based analysis,
  • reachability graph, analysis and visualisation,
  • coverability graph, analysis and visualisation,
  • explicite CTL model checking.

Charlie reads Petri nets in Snoopy and APNN format.

Charlie website


Marcie - (M)odel checking (A)nd (R)eachability analysis done effi(CIE)ntly


Qualitative and quantitative analyis of (Extended) Generalized Stochastic Petri nets including

  • Qualitative analysis, CTL model checking based on Interval Decision Diagrams (IDD),
  • Quantitative analysis, CSL model checking based on symbolic (IDD) exact numerical analysis,
  • Quantitative analysis, PLTLc model checking based on explicit approximative numerical analysis (FAU),
  • Quantitative analysis, PLTLc model checking based on simulation.

Marcie reads stochastic Petri nets in APNN*.

Marcie website


MC2


Simulative PLTLc model checking of stochastic or continuous traces. These traces can be simulation traces or logs from wetlab experiments.

MC2 reads, e.g., stochastic and continuous simulation traces generated with Snoopy.

MC2 website


latest update: December 08, 2011, at 03:09 PM