Stochastic semantics The stochastic semantics is represented through a continuous-time Markov chain (CTMC), whose transient evolution can be given via the Chemical Master Equation (CME) (Kampen 1992). Let \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$C=(\varLambda ,R)$$\end{document}C=(Λ,R) be a CRN. The propensity rate \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\alpha _{\tau }$$\end{document}ατ of a reaction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\tau$$\end{document}τ is a function of the current configuration of the system x such that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\alpha _{\tau }(x)dt$$\end{document}ατ(x)dt is the probability that a reaction event occurs in the next infinitesimal interval dt. We assume mass action kinetics, therefore \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\alpha _{\tau }(x)=k_{\tau } \frac{\prod _{i=1}^{|\varLambda |} r_{i,\tau } ! }{N^{|r_{\tau }|-1}}\prod _{i=1}^{|\varLambda |} \left( {\begin{array}{c}x(\lambda _i)\\ r_{i,\tau }\end{array}}\right),$$\end{document}ατ(x)=kτ∏i=1|Λ|ri,τ!N|rτ|-1∏i=1|Λ|x(λi)ri,τ, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$r_{i,\tau }$$\end{document}ri,τ is the i-th component of the vector \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$r_{\tau }$$\end{document}rτ and \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$|r_{\tau }|=\sum _{i=1}^{|\varLambda |}r_{i,\tau }$$\end{document}|rτ|=∑i=1|Λ|ri,τAnderson and Kurtz (2011). We define a time-homogeneous CTMC \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$(X^C(t),t \in {\mathbb {R}}_{\ge 0})$$\end{document}(XC(t),t∈R≥0) with state space \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$Q \subseteq {{\mathbb {N}}}^{|\varLambda |}$$\end{document}Q⊆N|Λ| as follows. Given \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$x_0 \in Q$$\end{document}x0∈Q, where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$x_0$$\end{document}x0 is the initial configuration of the system, then \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$P(X^C(0)=x_0)=1$$\end{document}P(XC(0)=x0)=1. The transition rate from state \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$x_i$$\end{document}xi to state \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$x_j$$\end{document}xj is defined as \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$r(x_i,x_j) =\sum _{\{\tau \in R | x_j=x_i+ v_{\tau }\}} N\alpha _{\tau }(x_i)$$\end{document}r(xi,xj)=∑{τ∈R|xj=xi+vτ}Nατ(xi). \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$X^C(t)$$\end{document}XC(t) describes the stochastic evolution of the molecular populations of each species in C at time t. For \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$x \in Q$$\end{document}x∈Q, we define \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$P^{(t)}(x)=P(X(t)=x|X(0)=x_0)$$\end{document}P(t)(x)=P(X(t)=x|X(0)=x0), where \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$x_0$$\end{document}x0 is the initial configuration. The CME describes the time evolution of X as:2\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\begin{aligned} \frac{\rm d}{{\rm d}t} \left( P^{(t)}(x)\right)= & {} \sum _{\tau \in R} \left\{ N\alpha _{\tau }(x-\upsilon _{\tau })P^{(t)}(x-\upsilon _{\tau })-N\alpha _{\tau }(x)P^{(t)}(x)\right\} . \end{aligned}$$\end{document}ddtP(t)(x)=∑τ∈RNατ(x-υτ)P(t)(x-υτ)-Nατ(x)P(t)(x).The solution of the CME is computed through numerical simulation or discretisation techniques such as uniformization (Kwiatkowska et al. 2007), and is generally feasible only for small populations. The CTMC is often represented as a \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$Q \times Q$$\end{document}Q×Q rates matrix, which can be viewed as a state transition graph and subjected to model checking against temporal logic properties (Kwiatkowska et al. 2011).