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.
(1) Run: git submodule update --init --recursive (2) Obtain required dependencies by running get_dep.dev.sh (3) Use build_debug.sh to run StocHy in development mode
(1) Obtain required dependencies by running get_dep.dist.sh (2) Use build_release.sh to run StocHy
Unless opting to extend or connect StocHy with your own tools, it is advised to opt to install the release version.
All the built and compiled binary files are then found within /build/bin. One can then run the corresponding binary files by using ./stochy_XX where XX is the corresponding model name.
To facilitate sharing of StocHy between different operating environments we provide a docker container containing StocHy. Details are found within the Docker folder.
NOTE: this is currently no longer maintained
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
Example 3 Scaling in continuous dimensions
Example 4 Simulation of shs
Simply create your own Case_study.cpp file within /src/case_studies/. This follows the same structure as described within the TACAS paper, however we don't need to modify the main file each time. We now create an individual case study and call the case study we want to run.
All the src files for the individual libraries can be found within src/ . These are built as individual libraries and one can simply use any of the libraries as needed for further extensions.
(1) shs - contains the general model description for constructing a shs based on the input model structure; together with the simulator for shs.
(2) FAUST - library for performing abstractions via MDPs
(3) bmdp - library for performing abstractions via IMDPs
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.
A video demo of StocHy can be found at OxCAV