Snoopy

Category Cross-Omics>Pathway Analysis/Gene Regulatory Networks/Tools and Cross-Omics>Agent-Based Modeling/Simulation/Tools

Abstract Snoopy is a unifying Petri net framework that can be used to investigate biomolecular networks. It can be used to model and execute (animate/simulate) hierarchical graph-based system descriptions.

The tool comes with several pre-fabricated graph classes (in particular, different kinds of Petri nets and other related graphs), and facilitates a comfortable integration of further graph classes due to its generic design.

To support aspect-oriented model engineering, different graph classes may be used simultaneously.

Snoopy is currently being used for the verification of technical systems, especially software-based systems, as well as for the validation of ‘natural systems’, such as, metabolic pathways, signal transduction pathways and Gene Regulatory Networks (GRNs).

Snoopy Basic Capabilities --

1) Extensible - generic design facilitates for the add on of new graph types;

2) Adaptive - simultaneous use of several graph types; and the Graphical User Interface (GUI) adapts dynamically to the graph type in its active window;

3) Platform independent - Implementation: C++, wxWidgets, Xerces; and Windows, Mac OS X and Linux are supported.

Snoopy Main Features --

Hierarchies by sub-graphs; Logical (fusion) nodes; Different shapes for Net elements; Coloring of graph elements (e.g. paths or invariants); and the Automated layout by the GraphViz library;

Digital signature by the ‘md5 hash function’; Animation of place/transition Petri nets; Simulation of ‘stochastic/continuous’ Petri nets; Printing support: eps, Xfig, FrameMaker;

Import/export from/to analysis tools, (see ‘Related Software’ below...); SBML import/export (rules, events, functions Not supported); and Support of web-based Petri net animation.

Available Graph Classes --

Place/transition Petri net; Extended Petri net (read / inhibitor / reset arcs); Time(d) Petri net; Generalized stochastic Petri net; Continuous Petri net; Modulo Petri net; “Music” Petri net;

Reachability graph; MTBDD/MTIDD; Fault tree; Extended Fault tree; Freestyle net; EDL signature net; and Your favorite graph class.

Snoopy Related Software --

1) Charlie -- Charlie is a software tool that can be used to analyze ‘Place/Transition’ nets. It is currently being used for the verification of technical systems, especially software-based systems, as well as for the validation of natural systems, such as, metabolic pathways, signal transduction pathways and gene regulatory networks.

Charlie's Main Features -- Structural properties (net classes, deadlocks/traps); invariant based analysis (p- and t-invariants, dependent node sets);

Reachability graph based analysis - behavioral properties (boundedness, liveness, and reversibility), explicit Computational Tree Logic (CTL) model checking, explicit ‘Linear Temporal Logic (LTL) model checking’ and shortest paths; and Reachability/coverability graph visualization using the ‘JUNG’ library.

2) DSSZ-MC -- DSSZ-MC contains tools for the ‘symbolic analyses’ of bounded Petri nets for standard properties and CTL model checking. They are based on an efficient implementation of Zero-suppressed Binary Decision Diagrams (zbdd-mc) and Interval Decision Diagrams (idd-mc).

DSSZ-MC's Main Features -- No previous knowledge of the boundedness degree required (idd-mc); Efficient ‘saturation-based’ reachability analysis;

Dead state analysis with trace generation; Analysis of strongly connected components (liveness, reversibility);

Efficient ‘CTL model checking’ based on limited backward reachability analysis; and Support of Petri nets with extended arcs (read arcs, inhibitor arcs, reset arcs).

3) MC2(PLTLc) -- MC2(PLTLc) is a Monte Carlo Model Checker for properties written in Probabilistic Linear-time Temporal Logic with numerical constraints (PLTLc). The model checker takes as input a set of traces in the form of a simulation output file.

It also takes as input a query file containing a list of PLTLc properties, and returns for each property the probability that the set of traces satisfies the property.

MC2(PLTLc) can also calculate the ‘probabilistic domains’ of free variables within a property; thus it is easy to calculate the distribution of features, such as times at which peaks occur. MC2(PLTLc) can operate with stochastic/deterministic simulation output, deterministic parameter scan output or even Wet-lab data.

MC2(PLTLc) was developed at the Bioinformatics Research Centre at the University of Glasgow.

Features -- The main features of MC2(PLTLc) are:

Logic: Probabilistic Linear-time Temporal Logic with numerical constraints (PLTLc); Model Checking: Monte Carlo approximation through a finite number of finite traces; Probabilistic Domains: Computation of probabilistic domains of free variables in a PLTLc property;

Off-line approach: Any simulation output can be used, e.g. output from ODEs, SDEs, CTMC, Gillespie; Parallelizable: Traces can be evaluated in parallel, hence distributed computation;

Parameter Scan: Model checking over simulations with varying model parameters (initial concentrations or kinetic rate constants); and

Integrations: Able to read simulation output from Snoopy, Gillespie2, BioNessie and BioNessie Lite.

4) PInA -- PInA is a software tool for computation and analysis of ‘invariants’ of place/transition nets. It is currently being used for the verification of technical systems, especially software-based systems, as well as for the validation of natural systems, such as, metabolic pathways, signal transduction pathways and gene regulatory networks.

PInA's Main Features -- Computation of p- and t-invariants; Statistical analysis; Computation of dependent transition sets/MCT-sets; Cluster analysis; and Imports/exports from/to other tools.

5) INA -- INA - the Integrated Net Analyzer (see G6G Abstract Number 20608) - may be used to analyze Petri nets produced by Snoopy.

The tool has been developed at the Humboldt University in Berlin, Dept. of Computer Science; the “automata theory” over the last 20 years. So it shouldn't be a big surprise that INA only comes with a pure ‘ASCII user interface’.

6) Snoopy provides import(s) from the following tools/languages --

Petri net EDitor: PED; Abstract Petri Net Notation: APNN; TIme petri Net Analyzer: TINA; Systems Biology Markup Language Level 2 Version 3: SBML (rules, events and functions are Not supported as yet); and the ‘disjunctive normal form’ of a Boolean expression to a fault tree.

7) Furthermore, Snoopy provides export(s) to several analysis tools, among them --

McKit (The Model-Checking Kit); PROD (An Advanced Tool for Efficient Reachability Analysis); Maria (The Modular Reachability Analyzer); LoLA (a Low Level Petri net Analyzer); TINA (TIme petri Net Analyzer);

PEP (Programming Environment based on Petri Nets) (currently - export to ‘low level nets’ without a layout - only); BDD-based model checkers DSSZ-CTL and DSSZ-LTL; SBML Level 2 Version 3; and PRISM - a probabilistic symbolic ‘model checker’.

System Requirements

Contact manufacturer.

Manufacturer

Manufacturer Web Site Snoopy

Price Contact manufacturer.

G6G Abstract Number 20607

G6G Manufacturer Number 104207