Distributed Probabilistic-Control Hybrid Automata
Modelling and Model Checking Framework

> Description_

Distributed Probabilistic-Control Hybrid Automata (DPCHA) are a model for systems having discrete dynamics (such as computation and control), continuous dynamics (such as real-world physics), a changing number of participants, some of which may exhibit probabilistic behaviour.

Quantified Bounded Linear Temporal Logic (QBLTL) is a logic that we use for specifying properties of DPCHA, including support for (bounded) temporal operators and quantification and aggregation over the elements of the distributed system.

Statistical Model Checking (SMC) is an efficient (but unsound) verification technique that allows us to arbitrarily estimate the probability that a certain property of the system holds in a probabilistic system. We can use it to check important safety or efficiency conditions of a system modelled with DPCHA.

> Files_
. DPCHA Framework Source (zip)
. DPCHA Framework Library (jar)
. Smart Grid Case Study (link)
> Dependencies_
You will need the following libraries:
. Java Scientific Library, by Michael Thomas Flanagan (link)
. Stochastic Simulation in Java, by Pierre L'Ecuyer (link)
. JFreeChart/JFreeCommon, optional (link)
> Links_
< Main Page Case Study: Smart Grid >