Stochastic hybrid systems (shs) are a rich mathematical framework which capture the probabilistic relationship between discrete and continuous variables and their evolution in time.
StocHy is a C++ tool aimed at the modelling of stochastic hrybid systems together with their analysis, which takes the form of formal verification and control synthesis.
It targets the wider adoption of shs both in academia and in industry.
The tools allows to described discrete time shs by parsing well known state space models and allows for performing any of the following three tasks:
(1) simulation of stochastic processes (serving as a visualisation tool of shs)(2) formal verification via abstractions taking the form of Markov processes and their variants of interval Markov decision processes.(3) strategy synthesis for e.g. selection of control actions to maximise satisfiability of a certain property.
StocHy is an open-source tool. We welcome feedback, issues, bug-fixes, extensions to other existing tools and other enhancements.
The Stochastic Hybrid Systems tool : StocHy is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation v3.0.
The principal author of this tool is Nathalie Cauchi (also primary maintainer).
However, it is a malgamation of collaboration with Kurt Degiorgio, Sadegh Soudjani (author of FAUST^2 which inspired this work), Morteza Lahijanian (IMDP method), Luca Laurenti (IMDP method), Sofie Haesaert (Strategy synthesis via FAUST).
Please cite their relevant papers when using StocHy.
A tool paper describing the features of StocHy has been submitted to 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). A copy of the submission can also be found within the repository.