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.
Installation, documentation, and examples
Local dependencies (included with source)
External dependencies (use 'get_dep.h' to automatically install)
All the external dependies can be automatically installed using 'get_dep.sh'
boost, matio, armadillo, cubature, ginac, nlopt
Other dependencies assumed to be installed on the system
python2.7, numpy, matplotlib
Install the necessary dependencies by running the file 'get_dep.h'Clone the StocHy repositoryRun the 'run.sh' file (found within the make directory) which will automatically build and compile stochy
To facilitate sharing of StocHy between different operating environments we provide a docker container containing StocHy. This is called StocHyDocker.zip.
We maintain a wiki with all the installation details and running examples on how to use StocHy. This can be found at: Welcome
We provide four examples as part of StocHy. For each example we have a dedicated wiki page illustrating the examples and how to run them. The details are also found within the tool paper which can be found within this repository.
Example 1 Formal verification via IMDP or MDP method
Example 2 Strategy synthesis for obstacle avoidance
Simply modify the Main.cpp file to contain your model description and task selection. Then build and compile StocHy via ./run.sh within the make folder.
Benchmark for stochastic processes
We also provide a set of benchmarks for cyber-physical systems endowed with stochasticity (noise). These benchmarks serve as a means of constructing further models and test different verification/ synthesis
algorithms against models with different complexities.
The benchmarks can be found here, while the accompanying research paper describing these benchmarks can found is given here
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.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this toolbox (see LICENSE). If not, see https://www.gnu.org/licenses/.
It is the user's responsibility in assessing the correctness of the theory and software implementation before putting it to use in their own research or exploiting the results commercially. We are, however, very happy to answer any questions and investigate any bug reports.
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 the MDP method in this work), Morteza Lahijanian (IMDP method), Luca Laurenti (IMDP method), Sofie Haesaert (Strategy synthesis via FAUST).
Please cite their relevant papers when using StocHy.
The author is a DPhil student of Prof. Alessandro Abate within the group OxCAV.
A tool paper describing the features of StocHy will be presented at the 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.