Integrated Net Analyzer (INA)

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

Abstract The Integrated Net Analyzer (INA) is a program with whose help ‘Petri nets’ of very different kinds can be investigated under different firing rules (in particular timing) with regard to their general properties.

Typical properties which can be verified through the analysis are boundedness of places, liveness of transitions, and reachability of markings or states.

When modeling an existing or projected system in the language of Petri nets, the underlying abstraction process assigns certain properties of the system to properties of the net, e.g. the absence of deadlocks in the system can correspond to the non-reachability of a dead marking.

With this interactive, menu-driven program you can edit, reduce, execute and analyze nets. It comprises the analytical procedures offered in the earlier toolkits such as, Petri-Net-Machine, PAN, CPNA, and ATNA.

In essence, INA is a tool package supporting the analysis of Place/Transition Nets (Petri Nets) and Colored Petri nets.

INA combines the following:

1) A textual editor for nets;

2) A by-hand simulation part;

3) A reduction part for Place/Transition-nets;

4) An analysis part to compute:

These are then used to verify properties like boundedness, liveness, reversability, etc.

5) A model checker for Computational Tree Logic (CTL).

The editor gives you the possibility to construct and edit nets. You can use any graphical editor, too, if you know the structure of its database file, by writing a program which converts it to the INA-file format.

The by-hand simulation part gives you the ability starting at a given marking to ‘forward fire’ either single transitions or maximal steps; you can thus traverse parts of the ‘reachability graph’.

The reduction part can be used to reduce the size of a net (and of its reachability graph) while preserving liveness and boundedness.

The analysis can be carried out under different ‘transition rules’ (normal, safe, under capacities), with or without priorities or time restrictions (three types), and under the firing of single transitions or maximal sets of concurrently enabled transitions.

The analysis part contains a small Expert System which infers - from the known properties - further properties of the given net.

The structural information computed includes:

Conflicts (static, dynamic) and their structure (e.g. free choice property); Deadlocks and traps (deadlock-trap-property); and State machine decomposition and covering.

For certain subclasses of nets, these properties can be used to deduce ‘dynamic properties’.

‘Invariant analysis’ can be done by computing ‘generator sets’ of all place/transition invariants and of all non-negative invariants. Vectors can be tested for invariance properties.

For checking boundedness and coverability, the ‘coverability graph’ of the actual net can be computed using either the Karp-Miller algorithm or Finkel’s method.

For bounded nets, the ‘reachability graph’ can be computed and analyzed for liveness, reversability, dynamic conflicts, realizable transition invariants, livelocks, etc.

The symmetries of the given net can be computed and used to reduce the size of the reachability graph. It is also possible to apply stubborn reduction. Formulas expressed in Computational Tree Logic (CTL) - built using state predicates - can be checked.

Furthermore, ‘minimal paths’ can be computed, and the non-reachability of a marking can be decided.

No restrictions are imposed on the size of the net, except, of course, the RAM-capacity of the computer being used.

During a session, all commands and options are saved to a command file, so that the session can be repeated automatically with a different net.

Additional INA tools inatcl and TkINA --

INA is Not directly usable as a ‘computing engine’ for other applications (it is Not possible to invoke algorithms from outside this program) and it does Not provide a Graphical User Interface (GUI). Therefore, inatcl and TkINA were developed.

inatcl - inatcl is a Tcl-based interface to functionality provided by INA. It allows you to write simple applications using the interpreted scripting language Tcl.

TkINA - TkINA provides a graphical interface for starting analysis algorithms; some results are displayed in a textual format. It is integrated into the PEP tool (Programming Environment based on Petri Nets) and does Not provide its own graphical editor.

Within the PEP tool it can be used to generate and highlight, e.g. invariants, deadlocks, and state machine components. Nevertheless, TkINA can also be used as a standalone tool.

The following are (some) external graphical editors and tools that can export nets to INA --

1) PEP - (see G6G Abstract Number 20609) - The PEP tool (Programming Environment based on Petri Nets) is a comprehensive set of modeling, compilation, simulation and verification components, linked together within a Tcl/Tk-based graphical user interface.

2) Snoopy - (see G6G Abstract Number 20607) - Snoopy is a tool that can be used to model and execute (animate/simulate) hierarchical graph-based system descriptions.

3) Petri Net Kernel - The Petri Net Kernel provides an infrastructure for bringing ideas for analyzing, for simulating, or for verifying Petri Nets into action; namely, for integrating the idea into a tool.

And perhaps many other editors/tools Not mentioned here.

INA Documentation --

The manufacturer provides an extensive User Manual.

System Requirements

Contact manufacturer.

Manufacturer

Manufacturer Web Site Integrated Net Analyzer (INA)

Price Contact manufacturer.

G6G Abstract Number 20608

G6G Manufacturer Number 104208