Fast Parametric Model Checking through Model Fragmentation

Parametric model checking (PMC) is a formal technique for the symbolic analysis of Markov chains whose transition probabilities are specified as rational functions over a set of continuous variables [1, 3, 2]. Formally, a parametric discrete-time Markov chain is a tuple $D=(S,s_{0},\textbf{P},L),$ where: $S$ is a finite set of states; $s_{0}\in S$ is the initial state;$\textbf{P}:S\times S\rightarrow[0,1]$ is a transition probability matrix such that for any states $s,s^{\prime}\in S$, $\textbf{P}(s,s^{\prime})$ gives the probability of transitioning from $s$ to $s^{\prime}$, and, for any $s\in S$, $\sum_{s^{\prime}\in S},\textbf{P}(s,s^{\prime})=1$; $L:S\rightarrow 2^{\mathit{AP}}$ is a labelling function that maps every state $s\in S$ to elements of a set of atomic propositions $\mathit{AP}$ that hold in that state. A state $s\in S$ is absorbing if $\textbf{P}(s,s)=1$ and $\textbf{P}(s,s^{\prime})=0$ for all $s\neq s^{\prime}$, and a transient state otherwise.

When used in software performance and reliability engineering, the pDTMC states map to relevant configurations of the modelled system; and pDTMC transitions capture possible transitions between those states, corresponding to the feasible changes between their associated configurations. PMC is supported by the probabilistic model checkers PARAM [13], PRISM [14] and Storm [15]. These tools compute closed-form formulae for pDTMC properties specified in probabilistic computation tree logic (PCTL) [16, 17, 18] and defined (as in probabilistic model checking [19, 20, 21, 22, 23]) by the grammar:

where $\Phi$ is a state formula and $\Psi$ is a path formula, $k\in\mathbb{N}_{>0}$ is a timestep bound and $\alpha\in AP$ is an atomic proposition.

The PCTL semantics is defined using a satisfaction relation $\models$ over the states $S$. Given a state $s$ of a Markov chain $D$, $s\models\Phi$ means “$\Phi$ holds in state $s$”, and we have: always $s\models true$; $s\models a$ iff $a\in L(s)$; $s\models\neg\Phi$ iff $\neg(s\models\Phi)$; and $s\models\Phi_{1}\wedge\Phi_{2}$ iff $s\models\Phi_{1}$ and $s\models\Phi_{2}$. The time-bounded until formula $\Phi_{1}\,\mathrm{U}^{\leq k}\,\Phi_{2}$ holds for a path iff $\Phi_{1}$ holds in the first $i<k$ path states and $\Phi_{2}$ holds in the $(i+1)$-th path state; and the unbounded until formula $\Phi_{1}\,\mathrm{U}\,\Phi_{2}$ removes the bound $k$ from the time-bounded until formula. The next formula $X\Phi$ holds if $\Phi$ is satisfied in the next state. The state formula $\mathcal{P}_{\!=?}[\Psi]$ specifies the probability that paths starting at a chosen state $s$ satisfy a path property $\Psi$. Reachability properties $\mathcal{P}_{\!=?}[\mathsf{true}\,\mathrm{U}\,\Phi]$ are equivalently written as $\mathcal{P}_{\!=?}[\mathsf{F}\,\Phi]$ or $\mathcal{P}_{\!=?}[\mathsf{F}\,R]$, where $R\!\subseteq\!S$ is the set of states in which $\Phi$ holds. For a full description of the PCTL semantics, see [17, 16].

We summarise the concept of a pDTMC fragment and its exploitation by the PMC approach introduced in [4], where the results from this section are taken from. As shown in Fig. 2, a fragment of a pDTMC $D=(S,s_{0},\textbf{P},L)$ is a tuple

where: $Z\subset S$ is a subset of transient MC states; $z_{0}$ is the (only) input state of $F$, i.e., $\{z_{0}\}\!=\!\{z\!\in\!Z\mid\exists s\!\in\!S\!\setminus\!Z\>.\>\mathbf{P}(s,z)>0\}$; $Z_{\mathsf{out}}=\{z\in Z\mid\exists s\in S\setminus Z\>.\>\mathbf{P}(z,s)>0\}$ is the non-empty set of output states of $F$, and all outgoing transitions from the output states are to states outside $Z\setminus\{z_{0}\}$, i.e., $\mathbf{P}(z,z^{\prime})=0$ for all $(z,z^{\prime})\in Z_{\mathsf{out}}\times(Z\setminus\{z_{0}\})$.

Fragments are not strongly connected components (SCCs) of the graph induced by the pDTMC²² 2 i.e., the directed graph comprising a vertex for each pDMTC state and an edge between each pair of vertices that correspond to pDTMC states between which a transition is possible states and transitions. For instance, the “inner states” region of the fragment from Fig. 2 can contain one or more SCCs, and an outgoing transition from an output state in $Z_{\mathsf{out}}$ can reach a state $s$ comprising an outgoing transition back to the input state $z_{0}$. Any subset of model states satisfying the constraints described earlier in this section form a fragment. However, partitioning a pDTMC or a part of a pDTMC into fragments is not always possible. For example, fully connected subsets of states cannot be split into fragments because none of their states can be an inner fragment state (as shown in Fig. 2) as it will have incoming transitions from outside states and outgoing transitions to outside states; restructuring using the techniques described later in Section IV-B is not possible either, as the premises for these techniques are violated.

The theoretical framework from [4] shows that, if a fragment $F$ of a pDTMC $D$ is identified, then the “monolithic”, one-step PMC of reachability, unbounded until and (not covered in our paper) reward properties [24] of $D$ can be replaced by the following equivalent steps:

1. 1.

   Compute PMC formulae for the probabilities of reaching all the output states of fragment $F$ starting from its input state $z_{0}$; this amounts to the PMC of $\#Z_{\mathsf{out}}$ reachability properties of a pDTMC built from $F$ removing the incoming transitions of $z_{0}$ and by replacing the outgoing transitions of each output state in $Z_{\mathsf{out}}$ with a “self-loop” transition of probability $1$.

2. 2.

   Build an abstract pDTMC model $D^{\prime}$ from $D$ by replacing the states in $Z$ and their internal transitions with a single state $z^{\prime}$ whose incoming transitions (and transition probabilities) are those of $z_{0}$. Additionally, state $z^{\prime}$ has outgoing transitions to every state that one or more states from $Z_{\mathsf{out}}$ have outgoing transitions to in $D$; and the probabilities of these transitions can be expressed in terms of the reachability properties computed in step 1. Due to space constraints, we do not provide the expressions for these transition probabilities in the paper; the interested reader can find them in [4].

3. 3.

   Compute the PMC formula for the original property under analysis, for the abstract model from step 2.

4. 4.

   Combine the PMC from step 1 and the PMC formula from step 3 into a system of equations.

The system of equations from step 4 provides a closed-form analytical model for the analysed property. This analytical model is equivalent to the PMC formula obtained by analysing the original pDTMC in one step.

Because the PMC analyses from steps 1 and 3 are performed on models that are smaller and simpler than $D$, this four-step PMC approach is often faster, produces much simpler closed-form expressions, or succeeds for more complex models than monolithic PMC can handle. However, no method for partitioning pDTMCs into fragments is proposed in [4]. Instead, the approach is only exploited for specific types of component-based systems (i.e., service-based systems and multi-tier architectures) for which: (i) pDTMCs can be obtained by combining manually pre-built pDTMC models of their components; and (ii) the component pDTMCs form fragments in the system pDTMC. This limits the applicability of the approach (to specific types of systems for which new pDTMCs are assembled following this recipe), requires additional effort and expertise, and can be error prone due to the manual steps involved.

The fPMC partition of a pDTMC into fragments is performed by function Fragmentation from Algorithm 1. This function takes three arguments:

• $\bullet$

  the graph $\mathcal{G}(V,E)$ induced by the pDTMC;

• $\bullet$

  the set of states $R$ whose reachability $\mathcal{P}_{=?}[\mathsf{F}\;R]$ is being analysed;

• $\bullet$

  a threshold parameter $\alpha\geq 1$ whose role is described below,

and returns a set of pDTMC fragments $\mathit{FS}$, i.e., a set of tuples with the structure from Equation (2). As not all pDTMC states can be included into a fragment that follows the definition from Section II-B (e.g., states whose only outgoing transition is a self-loop transition do not satisfy the constraints associated with any type of fragment state), we extend this definition to include single-state fragments $F\!=\!(\{s\},s,\{s\})$ for any pDTMC state $s$.

The algorithm starts by placing into $\mathit{FS}$ single-state fragments for each state in the reachability set $R$ (line 2). We preserve the elements of $R$ as single-state fragments so they end up as states in the fPMC abstract model (see Fig. 1 and the description from Section II-B), so the reachability property $\mathcal{P}_{=?}[\mathsf{F}\;R]$ (which refers to these states) can be analysed for the abstract model. Next, the algorithm generates additional fragments in each iteration of the for loop from lines 3–25 as follows. First, a node $z_{0}$ not yet included in any fragment is selected³³ 3 The selection order for $z_{0}$ has an impact on the fragmentation of the pDTMC, and thus on its parametric model checking time; however, finding the best selection order is outside the scope of this paper. (line 3) and inserted into the fragment state set $Z$, while the fragment output set $Z_{\mathsf{out}}$ is initialised to the empty set (line 4). A stack $T$ is then populated with the states reached by outgoing transitions from $z_{0}$ by invoking (in line 6) the function Traverse from Algorithm 2. Each state $w$ from this stack is processed by the while loop from lines 7–19, ending up in $Z_{\mathsf{out}}$ if it satisfies the constraints associated with output fragment states (lines 9 and 10). When $w$ does not satisfy these constraints, two options are possible (lines 12–16):

• $\bullet$

  If $Z$ has accumulated fewer states than the threshold $\alpha$, the graph traversal function Traverse is invoked again to add to the stack the predecessor and successor vertices of $w$ that are not already in the fragment (line 13).

• $\bullet$

  Otherwise, a restructuring of the graph (see Section IV-B) is invoked (line 15) to “force” $w$ into becoming an output state, and thus to enable the formation of a fragment.

In this way, the threshold $\alpha$ provides a soft upper bound for the fragment size, deciding whether fPMC will continue model traversal (adding states into the stack) or attempt model restructuring by forcing the currently analysed state to become an output state. As the result, a larger $\alpha$ is expected to lead to larger fragments. When this bound, $\alpha$, is reached, the model restructuring techniques detailed in Section IV-B are used to force the formation of a valid fragment. The fragment candidate $(Z,z_{0},Z_{\mathsf{out}})$ finalised by the while loop is then “downgraded” to a single-state fragment if it does not meet the definition from Section II-B (lines 20–22), after which it is added to the fragment set $\mathit{FS}$ (line 23). Additionally, the states $Z$ of this fragment are added to the set $R$ of states already assigned to fragments (line 24), ensuring that the loop starting in line 3 does not reuse them to form other fragments.

Finally, the Traverse function from Algorithm 2 takes a vertex $w$ and examines its incoming edges (if $w$ is not the initial fragment state $z_{0}$, lines 2–11), and its outgoing edges (at all times, lines 12–21). Vertices connected to $w$ by these incoming and outgoing edges and not already in the set of fragment states $Z$ are collected into the input vertex set $I$ (line 3) and output vertex set $O$ (line 12), respectively. The former are then added to the stack $T$ if none of them belongs to an existing fragment (lines 4 and 5). Otherwise, the non-input vertex $w$ has incoming edge(s) from another fragment, violating the condition that incoming transitions to inner and output fragment states are only allowed from states within the same fragment; hence, $w$ becomes a single state fragment and the graph traversal is terminated (lines 6–9). Lastly, if the output set $O$ has at least a vertex not in other fragments (line 13), growing the fragment under construction with $w$’s successors may be feasible, and thus the for loop in lines 14–21 places the $O$ vertices not in other fragments on the stack $T$ (line 16) and attempts to restructure the graph to allow fragment formation if these vertices are already part of other fragments (line 18).

Due to space constraints, the full analysis of Algorithms 1 and 2 is provided as supplementary material on our project webpage. Here, we note that the algorithms are guaranteed to produce a set of valid fragments, comprising: (i) the degenerate, single-state fragments created in lines 2 and 21 of Fragmentation and in line 7 of Traverse; (ii) the fragments that “pass” the validation from line 20 of Fragmentation, which we assume correct. Furthermore, both algorithms terminate. Traverse terminates because each of its statements (including the assembly of the vertex sets $I$ and $O$, and its only for loop) operate with a finite number of vertices. Fragmentation terminates because: (i) each iteration of its for loop adds at least one vertex (i.e., $z_{0}$) to $R$ in line 24 until $V\setminus R=\{\}$ in line 3 (since $V$ is a finite set) and the loop terminates; (ii) its while loop terminates since it iterates over the elements of stack $T$ that can only contain one instance of vertices from the finite set $V$ and is therefore finite too; and (iii) Restructure invocations can only add a finite number of vertices to $V$, as we show in the next section.

While the model fragmentation from §IV-A is guaranteed to produce valid fragments, the success of fPMC also depends on these fragments being neither too small nor too large. Small fragments may yield a large abstract model that may be unfeasible to analyse using standard PMC (Fig. 1); however, in our experience, the pDTMCs whose PMC we want to speed up comprise many loops (cf. Fig 5) that preclude the formation of only small fragments. In contrast, fragments that are too large for standard PMC are more likely to be obtained. As such, fPMC uses the threshold $\alpha$ to decide when to attempt to force the formation of a fragment in line 15 from Algorithm 1, and further attempts to enable fragment formation in line 18 from Algorithm 2, in the two scenarios below.

1) When a state $z$ of a fragment under construction has both outgoing transitions to inner fragment states and $n\geq 1$ outgoing transitions (of probabilities $p_{1}$, $p_{2}$, …, $p_{n}$) to states $s_{1}$, $s_{2}$, …$s_{n}$ not in the fragment (Fig 6(a), left). In this case, the addition of one auxiliary state $z^{\prime}_{i}$ for each outgoing transition to a state $s_{i}$, $i=1,2,\ldots,n$ (Fig 6(a), right) enables the formation of a fragment that includes the auxiliary states as output states. Each auxiliary state $z^{\prime}_{i}$ has an incoming transition of probability $p_{i}$ from state $z$, and an outgoing transition of probability $1$ going to state $s_{i}$.⁴⁴ 4 Using a single auxiliary state $z^{\prime}$ obtained by combining states $z^{\prime}_{1}$, $z^{\prime}_{2}$, …, $z^{\prime}_{n}$ is also possible, but leads to more complex expressions for the new transition probabilities, so we did not opt for it in the current version of fPMC.

2) When a non-input state $z$ of a fragment under construction has $m\geq 1$ incoming transitions (of probabilities $p_{i1}$, $p_{i2}$, …, $p_{im}$) from states $s_{i1}$, $s_{i2}$, …$s_{im}$ outside the fragment, and $n\geq 1$ outgoing transitions (of probabilities $p_{o1}$, $p_{o2}$, …, $p_{on}$) to states $s_{o1}$, $s_{o2}$, …$s_{on}$ not in the fragment (Fig 6(b), left). In this case, each of the $m$ transitions from a state $s_{ij}$ to $z$, $j=1,2,\ldots,m$, can be replaced by $n$ transitions from state $s_{ij}$ to states $s_{o1}$, $s_{o2}$, …$s_{on}$ (Fig 6(b), right), where the probability of transition from $s_{ij}$ to $s_{ok}$, $k=1,2,\ldots,n$, is set to $p_{ij}p_{ok}$.

Note that the restructuring process is invoked halfway through the construction of a fragment, when $Z_{\mathsf{OUT}}$ has not yet been finalised. Thus, the model restructuring process can apply to any state $z$ that satisfies one of the above scenarios and that we may want to include into $Z_{\mathsf{OUT}}$, but cannot because one of the constraints from the definition of a fragment is violated.

From the two model restructuring techniques, only the first increases the number of pDTMC states – with as many auxiliary states as there are ougoing transitions from state $z$ to states outside the fragment under construction. Because (i) the pDTMC has a finite number of states, each with a finite number of outgoing transitions; and (ii) the auxiliary states do not require the application of the first technique (as they have a single outgoing transition), it follows that the maximum number of auxiliary states that fPMC may create is also finite.

Applied to the pDTMC and reachability property for the FX system from our running example (which current parametric model checkers cannot analyse, cf. §III), our fPMC tool (run for $\alpha=6$) generated the model fragmentation from Fig. 7. The five single-state and eight multi-state fragments (13 fragments in total) comprise 49 states and 83 transitions compared to the 29 states and 58 transitions of the original pDTMC (Fig. 5), with the additional states and transitions due to the model restructuring techniques from §IV-B. The end-to-end computation of a closed-form analytical model for the FX success probability took fPMC 4.43s, and the algebraic formulae of this model contain 1,456 arithmetic operations and took 0.002s to evaluate in Matlab (on a computer with the specification from Section VI-B). As for all fPMC experiments presented in the paper, we carefully checked the correctness of our PMC formulae by ensuring that their evaluation for randomly generated combinations of parameter values produced the same numerical results (subject to negligible rounding errors) as those obtained by running the probabilistic model checkers PRISM [14] and Storm [15] to analyse the non-parametric Markov chains obtained by replacing the pDTMC parameters with these random values.

We carried out experiments to answer the following three research questions (RQs).

We evaluated fPMC for three software systems and processes taken from related research [4, 5, 27, 28, 25] and belonging to different application domains. We selected these systems because (i) their Markov models include hyperparameters that can be tuned to devise pDTMCs with various numbers of states $S$ and transition probability matrices P; and (ii) without changing the pDTMC structure, several non-trivial transition probabilities in P can become parameters, thus increasing the number of parameters within the model. Due to space constraints, we only provide brief descriptions of these systems; full details are available from [4, 5, 27, 28, 25].

• SEQ:

  The services are invoked in order, stopping after the first successful invocation or after the last service fails.

• PAR:

  All services are invoked in parallel (i.e., simultaneously), and the operation uses the result returned by the first service terminating successfully.

• PROB:

  A probabilistic selection is made among the available services with the total probability being equal to 1.

• PROB_R:

  Similar to PROB, but if the selected service fails, it is retried with a given probability (as in SEQ_R).

We compare fPMC against the leading PMC model checkers PRISM (version 4.6) and Storm (version 1.5.1), both with their default settings. For a fair comparison, we ensured that both PRISM and Storm can process at least the simpler pDTMCs of these systems. We run each experiment using fPMC, PRISM and Storm, and observe (i) the time required to compute the PMC formulae, with a 60-minute timeout (the lower the execution time the better); and (ii) the number of arithmetic operations in the devised formulae (formulae with fewer arithmetic operations can be evaluated faster).

All experiments were performed on a MacBook Pro (early 2015) with 2.7GHz dual Core Intel i5 processor and 8GB RAM. The source code, the full Markov models and reachability properties, and all experimental results are publicly available at https://github.com/xinwei2124/fPMC_ICSE.

For all pDTMCs of FX variants, fPMC succeeded in computing all closed-form formulae within the 60 minutes timeframe (fPMC column) taking $2.5s$ for the simplest models, and just under 240s for most models with the exception of SEQ_R with 5 services for which fPMC took $\approx\!1560s$. In contrast, Storm computed the formulae for eight of 21 pDTMCs ($\approx\!38\%$) with the majority being the simplest models across all execution strategies, except from PROB variants for which Storm produced all formulae. Finally, PRISM computed the PMC formulae for four of the 21 pDTMCs ($\approx\!20\%$), which again were the pDTMCs with the fewest states and transitions.

Similar results were obtained for the four analysed PL system variants (with 4, 16, 18 and 22 features) whose results are shown in Table II. Considering column P100, for instance, the most difficult case in which the transition probability matrix P comprises only parameters (i.e., no transition is set to a constant value), fPMC returned the closed-form formulae in less than $\approx\!\!94s$ in the worst case. Neither Storm nor PRISM succeeded in any of the four PL system variants for $P100$.

While fPMC outperforms both Storm and PRISM when handling complex models with several parameters, we noticed an interesting behaviour with simpler models (for FX and PL) and simpler properties (for COM). In particular, for the simplest FX models with SEQ, PAR and PROB strategies and 1–2 services (cf. Table I) mostly Storm, and occasionally PRISM, computed the formulae faster than fPMC. This behaviour occurs for PL system models up to $P40$ in Table II ($40\%$ of the total pDTMC parameters were maintained) and properties $P1\!\!-\!\!P7,P16\!\!-\!\!P21$ for the COM process (Table III). Since both Storm and PRISM represent internally the induced pDTMCs with advanced data structures (e.g., sparse matrices, binary decision diagrams) and use sophisticated reachability analysis algorithms, this behaviour is logical for models and reachability properties that can exploit these features. As we have demonstrated, however, these features alone cannot handle reachability properties for pDTMCs with characteristics similar to those of the most complex models in Tables I–III. This observation indicates the potential of a hybrid probabilistic model checker that uses fPMC and Storm/PRISM interchangeably based on the pDTMC structure and reachability property.

Considering the complexity of the derived closed-form formulae as a factor of the number of involved arithmetic operations, we observe that for all systems and all variants, the complexity increases as the model complexity (states and transitions) increases. For instance, for the FX system with SEQ_R strategy (the motivating example) the arithmetic operations for the fPMC-computed formulae increase from 3068 to $\approx\!386\!K$ as the number of functionally-equivalent services increases from two to five. In general, the fPMC-produced formulae contain fewer operations than those produced by Storm or PRISM. This observation is evident in Table III, where the closed-form analytical models derived from fPMC include $98K\!\!-\!\!208K$ operations for all properties, whereas, in many cases, the formulae produced by Storm and PRISM are very large (between several megabytes and 167MB) and could not be analysed using our experimental machine.

These findings indicate that fPMC, underpinned by the model fragmentation algorithm, significantly speeds up the parametric model checking of reachability properties by several orders of magnitude, produces closed-form analytical models of modest complexity, and enables the analysis of pDTMCs that leading probabilistic model checkers cannot handle. Also, the use of systems from different application domains, whose induced pDTMCs have distinct characteristics in terms of model structure and complexity, provides evidence supporting the general applicability of fPMC. This conclusion is reinforced by the fact that the fragmentation is completely automated and does not require any domain knowledge or human intervention (cf. Algorithms 1 and 2).

Table II shows the PMC results for the four PL variants. For all PMC approaches, as expected, increasing the number of pDTMC model parameters incurs a corresponding increase in the execution time and formulae complexity. Both Storm and PRISM, however, exhibit exponential growth in these two metrics until P60, and fail to produce any formula from P70 thereafter. In fact, some of the formulae comprise as many as 3.91M and 1.17M arithmetic operations for PRISM and Storm, respectively. In contrast, fPMC terminates successfully in all cases, consuming at most 94s, indicating that fPMC is barely influenced by the increase in model parameters. This insight is also supported by the result that the fPMC-computed closed-form analytical models contain at most 261K operations.

Considering these results, we have strong empirical evidence indicating that the higher the percentage of transition probabilities specified as rational functions over the total number of transition probabilities, the more apparent is the performance gap favouring fPMC over Storm and PRISM. Accordingly, fPMC can support the derivation of closed-form analytical models for reachability properties whose associated pDTMCs specify as much as 100% transition probabilities as rational functions in the evaluated pDTMCs.

We limit construct validity threats that may originate from simplifications and assumptions made when establishing the experimental methodology using the pDTMCs and reachability properties from three publicly-available software systems and processes, also used in related research [4, 5, 27, 28, 25].

We mitigate internal validity threats that could introduce bias when identifying cause-effect relationships in our experiments by designing independent research questions and evaluating the effectiveness, scalability and configurability (sensitivity) of fPMC. To further reduce the risk of biased results, we compared fPMC against the latest versions of the leading probabilistic model checkers Storm [15] and PRISM [14] that were available when we conducted the evaluation. We also performed experiments using multiple variants of the studied software systems and process, and evaluated the correctness of all the fPMC-computed formulae by adopting the approach described in Section IV-C. Finally, we enable replication and verification of our findings by making all experimental results publicly available online.

We limit external validity threats that could affect the generalisability of our findings by evaluating fPMC using pDTMCS of systems and processes from three different application domains (i.e., service-based systems [29, 30], software product lines [31, 32], communication processes [33, 34]). Furthermore, we carried out experiments to check that fPMC can work with pDTMCs containing up to 83 parameters, incurring modest increase in execution time with the computed closed-form analytical models containing significantly fewer arithmetic operations than those produced by the model checkers PRISM and Storm. We reduce further the risk that fPMC might be difficult to use in practice by developing an fPMC prototype tool that requires the same domain expertise for specifying pDTMCs as for using PRISM and Storm. However, additional experiments are needed to confirm that fPMC can analyse pDTMCs modelling other software systems and processes than those employed in our evaluation.