1: \begin{abstract}

2:   We consider the problem of verifying stochastic models of biochemical networks 

3:   against behavioral properties expressed in temporal logic terms. 

4:   Exact probabilistic verification approaches 

5:   such as, for example, CSL/PCTL model checking, are undermined by 

6:   a huge computational demand which rule them out for most real case studies. 

7:   Less demanding approaches, such as statistical model checking, estimate the likelihood  

8:   that a property is satisfied   by sampling   \emph{executions} 

9:   out of the stochastic model.  

10:   We propose a methodology for efficiently estimating the likelihood that a LTL property $\phi$ holds of a  

11:   stochastic model of a biochemical network. As with other statistical verification techniques, the methodology we propose 

12:   uses a stochastic simulation algorithm for generating execution samples, however there are three key aspects that improve the efficiency: 

13:   first, the sample generation is driven by on-the-fly verification of $\phi$ which results in optimal 

14:   overall simulation time. 

15:   Second, the confidence interval estimation for the probability of $\phi$ to hold is based on an efficient variant of 

16:   the Wilson method which ensures a faster convergence. Third, the whole methodology is   designed according to a parallel fashion and a prototype 

17:   software tool has been implemented that performs 

18:   the  sampling/verification process in parallel over an HPC architecture. 

19: \end{abstract}

20: