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

Tool Features

Petri Nets Supported (see also help on terminology) Components (see also help on terminology)


Tool Description

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.

Contact Information

B.F. Postema
University of Twente
Hallenweg 19
7522 NH Enschede
The netherlands

Phone:  +31534893885
E-mail: b.f.postema@utwente.nl

Other Remarks

[PN Home][*]
The maintainers of this page