Fluid Survival Tool
Entry last updated: 2014/7/9
Entry last validated: 2014/7/9
Tool homepage: https://code.google.com/p/fluid-survival-tool/
Tool availability: Free of charge
Petri Nets Supported (see also help on terminology)
Components (see also help on terminology)
- Stochastic Petri Nets
- Petri Nets with Time
- Simple Performance Analysis
- Advanced Performance Analysis
Hybrid Petri nets with a general one-shot transition (HPNG) allow to model systems with discrete and continuous quantities that follow mainly deterministic characteristics. An efficient partitioning for the underlying state-space of such Petri nets has been presented, namely the so-called Stochastic Timed Diagram (STD). This partitioning allows to compute the probability distribution to be in a certain state at a certain time in a very efficient way and avoiding discretization. Algorithms for model checking Stochastic Timed Logic (STL) allow to efficiently check complex and nested properties on the underlying STD. A probability operator is used to lift the logic which reasons on STDs to the level of the HPNG.
This tool allows to model HPNGs. The system generates with an input STL formula, using the region-based techniques of STDs, a verdict for a specific time or produces a probability distribution.
University of Twente
7522 NH Enschede
The maintainers of this page