Stochastic model checking is a formal technique by means of which formally stated properties of a discrete-state stochastic model can be automatically assessed (i.e. through an algorithm).
The expressive power of stochastic temporal logics (i.e. the formal languages employed to formally express the properties of a stochastic model) is a fundamental aspect in the realm of formal verification, characterising the ability of the modeller to
analyse (i.e understand) a model.
In this presentation we consider a recently introduced stochastic logic, namely the Hybrid Automata Stochastic Logic (HASL), which establishes a powerful framework to express sophisticated measures of a stochastic model.
We will look at the application of the HASL formalism into some biological oriented problem, more specifically: the analysis of the dynamics of a simple model of gene-expression with stochastic delayed dynamics, as well as the analysis of oscillatory trends in a simple sustained oscillator.