> Description_  
Distributed ProbabilisticControl Hybrid Automata (DPCHA) are a model for systems having discrete dynamics (such as computation and control), continuous dynamics (such as realworld 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_  
