Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Probabilistic model checking is an extension of the formal verification methods for systems exhibiting stochastic behaviour. The system model is usually specified as a state transition system, with probabilities attached to transitions, for example, Markov chains. A wide range of quantitative performance, reliability, and dependability measures can be specified using temporal logics such as Continuous Stochastic Logic (CSL) defined over Continuous Time Markov Chains (CTMC) [1] and Probabilistic Computational Tree Logic (PCTL) defined over Discrete Time Markov Chains (DTMC) [8]. To perform model checking by numerical analysis we need to compute transient-state or steady-state distribution of the underlying CTMC. The numerical model checking has been studied extensively and numerous algorithms [2] have been devised and implemented in different model checkers. Despite the considerable works in the domain, the numerical Markovian analysis still remains a problem.

Different approaches have been applied to overcome the state space explosion problem. Data structures which lead to compact representations of large models such as Binary Decision Diagrams (BDD) and Multi Terminal Binary Decision Diagrams (MTBDD) with efficient manipulation algorithms have been applied to consider large models. This approach is called symbolic model checking [3]. Another approach is based on the state space reduction techniques. The idea here is to have a representation of the underlying model in a reduced-size model, which is called abstraction in model checking [10]. The large models can also be analysed by decomposition which means that sub-systems are analysed in isolation and then the global behaviour is deduced from these solutions. This is called as compositional model checking [4, 6].

The goal of this paper is to present a model checking approach which is able to take advantage of product form solutions. It is worth pointing out that product form solutions play an important role in calculating stationary distributions of Markov chains in performance evaluation [1], but, on the contrary, are believed to have no significant use in model checking. In this paper, we study a subclass of Stochastic Automata Networks (SANs) without synchronisations, which have product form steady-state distributions [7]. In the subclass, there is no synchronisation, all transition rates are functional and restricted to satisfy a property that we call inner proportional. This class remains large enough, for example, to generalise competing Markov chains [5]. We profit from product form solutions of this class to perform the CSL model checking for the untimed Until path and the steady-state formulae.

The rest of the paper is organised as follows: Sect. 2 gives a brief introduction for CSL and then introduces the class of SANs for which the compositional model checking is performed. Section 3 proves the product form solution for the steady-state and Sect. 4 provides the product form over untimed paths.

2 Framework and Model

CSL Model checking: In this paper, we consider the steady-state and untimed Until formulae of CSL model checking. We briefly give the syntax and semantic for these operators and we refer to [1, 2] for further information. Model \(\mathcal M \) is a time-homogeneous CTMC with infinitesimal generator \(Q\) taking values in a set of states \(S\). \(AP\) denotes a finite set of atomic propositions, and \(L: S \rightarrow 2^{AP}\) is the labelling function which assigns to each state \(s \in S\) the set \(L(s)\) of atomic propositions \( a \in AP\) those are valid in \(s\). A path through \(\mathcal M \) can be finite or infinite. A finite path \(\sigma \) of length \(n\) is a sequence of states: \(\sigma =s^0,s^1,\ldots ,s^n\) with transition rates \(Q(s^i,s^{i+1})>0\). We denote by \(paths_{s}\) the set of all paths starting from state \(s\). Let \(p\) be a probability threshold and \(\triangleleft \) be an arbitrary operator in the set \(\{\le , \ge , < ,> \}\).The syntax of CSL is defined by :

$$\begin{aligned} \phi :\!{:}= true \mid a \mid \phi \wedge \phi \mid \lnot \phi \mid \mathcal P _{\triangleleft p}(\phi \,\,\mathcal U \,\phi ) \mid \mathcal S _{\triangleleft p}(\phi ) \end{aligned}$$

The expression \(\mathcal P _{\triangleleft p}(\phi _1 ~\mathcal U ~\phi _2)\) asserts that the probability measure of paths satisfying \(\phi _1 ~\mathcal U ~\phi _2\) meets the bound given by \(\triangleleft p\). The path formula \(\phi _1 ~\mathcal U ~\phi _2\) asserts that \(\phi _2\) will be satisfied at some time \(t \in [0, \infty )\) and that at all preceding time \(\phi _1\) holds. \(\mathcal S _{\triangleleft p}(\phi )\) asserts that the steady-state probability for \(\phi \)-states meets the bound \(\triangleleft p\). We present briefly the semantics of these formula where \(\models \) is the satisfaction operator:

  • \(s \models true\)                    for all \(s \in S\)

  • \(s \models a\)                         iff \(a \in L(s)\)

  • \(s \models \lnot \phi \)                      iff \(s \not \models \phi \)

  • \(s \models \mathcal P _{\triangleleft p}(\phi _1 ~\mathcal U ~\phi _2)\;\)    iff \(\mathbb P ^\mathcal{M }(s,\phi _1 ~\mathcal U ~\phi _2) \triangleleft p\)

  • \(s \models \mathcal S _{\triangleleft p}(\phi )\)                iff \( \sum\nolimits _{s | s \models \phi } \pi ^\mathcal{M }(s) \triangleleft p\)

where \(\mathbb P ^\mathcal{M }(s,\phi _1 ~\mathcal U ~\phi _2)\) denotes the probability measure of all paths \(\sigma \) starting from \(s\) (\(\sigma \in paths_{s}\)) satisfying \(\phi _1 ~\mathcal U ~\phi _2\), i.e., \(\mathbb P ^\mathcal{M }(s,\phi _1 ~\mathcal U ~\phi _2)= \mathbb P \{\sigma \in paths_{s} \mid \sigma \models \phi _1 ~\mathcal U ~\phi _2\}\); \(\pi ^\mathcal{M }(s)\) denotes the steady-state probability of state \(s\) of the chain \(\mathcal M \). In the case \(\mathcal M \) is ergodic, the steady-state distribution is independent of the initial state, then the steady-state formula is satisfied or not whatever the initial state.

SANs with local, functional and inner proportional transitions: Consider a network of \(N\) interacting stochastic automata \(A_1, A_2,\ldots A_N\) where

  • Transitions are local, i.e., not synchronised: it is forbidden to have two events occurring at the same time in two different automata.

  • Transition rates of each automaton depend on the state of the whole system. Such transitions are also called functional transitions.

  • For any automaton, transition rates are restricted to be inner proportional: they may depend on the state of all other automata; however, the proportion between two arbitrary transition rates of this automaton remains independent from the state of other automata.

In this work, we note

  • \(s=(s_1,s_2,\ldots ,s_N)\) the state vector, \(s_{-k}=(s_1,\ldots ,s_{k-1},s_{k+1},\ldots ,s_N)\) the state vector without component \(s_k.\)

  • \(\mathcal{{S}}_k\) the set of states of automaton \(A_k\), \(\mathcal{{S}}=\mathcal{{S}}_1\times \mathcal{{S}}_2\times \cdots \times \mathcal{{S}}_N\) the set of all system states, and \(\mathcal{{S}}_{-k}=\mathcal{{S}}_1\times \cdots \times \mathcal{{S}}_{k-1}\times \mathcal{{S}}_{k+1}\times \cdots \times \mathcal{{S}}_N\) the set of states of all automata other than \(A_k.\)

  • \(Q_k^s: \mathcal{{S}}_k\times \mathcal{{S}}_k \rightarrow \mathbb R \) the infinitesimal generator of \(A_k\) when the system is in state \(s\). More precisely, transition rates of \(A_k\) are functions of the state vector \(s_{-k}.\)

In state \(s\), the total outgoing rate from automaton \(A_k\) is \(-Q_k^s(s_k,s_k) = \sum\nolimits _{s^{\prime }_k\ne s_k} Q_k^s(s_k,s^{\prime }_k).\)

Property 1

(Characterisation of inner proportional transitions) The transition rates of \(A_k\) are inner proportional if and only if there exists a state-dependent factor \(\alpha _k: \mathcal{{S}}_{-k} \rightarrow \mathbb R \) and an infinitesimal generator \(Q_k:\mathcal{{S}}_k\times \mathcal{{S}}_k\rightarrow \mathbb R \) which does not depend on the vector \(s_{-k}\) such that

$$\begin{aligned} Q_k^s(s_k, s^{\prime }_k) = \alpha _k(s_{-k}) Q_{k}(s_k, s^{\prime }_k) \qquad \forall s_k,s_{k^{\prime }}\in \mathcal{{S}}_k, \forall s_{-k}\in \mathcal{{S}}_{-k}. \end{aligned}$$
(1)

Matrix \(Q_k\) is the infinitesimal generator of the representative automaton of \(A_k\) (or \(A_k\) in isolation). In isolation, the total outgoing rate from state \(s_k\) is given by \( -Q_k(s_k,s_k) = \sum\nolimits _{s^{\prime }_k\ne s_k} Q_k(s_k,s^{\prime }_k).\)

3 Product Form Solution for the Steady-State

First of all, SANs with local, functional and inner proportional transitions form a subclass of SANs without synchronisations considered in [7]. In this work, Fourneau et al. considered SANs where transitions are local and functional, but not necessarily inner proportional. They denote by \(F_k\) the set of infinitesimal generators of \(A_k\). This notation \(F_k\) denotes the set \(\{Q_k^s: s\in \mathcal{{S}}\}\) in our model. Theorem 6 of [7] states that a SAN with local and functional transitions has a product form steady-state distribution if for any automaton \(A_k\) there exists a probability distribution \(\pi _k\) that verifies the following equation

$$\begin{aligned} \pi _k Q = 0 \qquad \forall Q\in F_k. \end{aligned}$$
(2)

In the view of Property 1, for inner proportional transitions, \(F_k\) is given by

$$\begin{aligned} F_k = \{\alpha _k(s_{-k})Q_k: s_{-k}\in \mathcal{{S}}_{-k}\}, \end{aligned}$$

where \(\alpha _k\) is a real-valued function of \(s_{-k}\) and \(Q_k\) is the representative infinitesimal generator of automaton \(A_k\). Thus, a distribution \(\pi _k\) satisfies Eq. (2) for all infinitesimal generators of \(A_k\) if it satisfies the following Eq. (3) for only \(Q_k\).

Theorem 1.

If for each automaton \(A_k\) in isolation there exists a probability distribution \(\pi _k\) such that

$$\begin{aligned} \pi _k Q_k = 0, \end{aligned}$$
(3)

then the steady-state distribution of the system has the following product form

$$\begin{aligned} \pi (s) = C\prod _{k=1}^N \pi _k(s_k). \end{aligned}$$
(4)

This product-form solution can be used to check the steady-state formula \(\mathcal S _{\triangleleft p}(\phi )\) to see if the sum of steady-state probabilities of states satisfying \(\phi \) meets the bound \(p\) or not. In the following, two applications of this product form result will be illustrated.

Example 1

Generalised competing Markov chains. We extend the system of competition between concurrent processes over a number of shared resources [4, 5]. The extension is that common resources are no longer limited to be mutually exclusive and strong blocking but may be used by different components at the same time. In other words, transition rates may not be switched off to zero but are only reduced by some factor when common resources are shared. Transition rates are local, functional and inner proportional: when a component shares some common resources with others, its transition rates are reduced by some factor \(\alpha \), which might be a function of the states of all other resources. More precisely, the transition rate matrix of component \(k\) is of the form \( Q_k^s = \alpha _k(s_{-k}) Q_k. \) Thus, Theorem 1 applies to this system of generalised competing Markov chains.

Example 2

Multiclass queue with proportional state-dependent rates In this example, Theorem 1 is applied to a multiclass queue with state-dependent arrival rates and service rates. Consider a queue of \(N\) classes of customers where customers of each class arrive according to a variable-rate Poisson process. Let \(x_k\) be the number of class-\(k\) customers, \(x=(x_1\ldots x_N)\) be the system state. For class \(k\), suppose that service requirements follow an exponential distribution of parameter \(\mu _k\) and the arrival rate \(\lambda _k(x_{-k})\) is a general function of the vector \(x_{-k}\) composed of numbers of customers of other classes. Besides, suppose that the service effort \(\varPhi _k(x_{-k})\) allocated to class \(k\) is also a function of \(x_{-k}.\) Thus, class \(k\) is characterised by state-dependent arrival rate \(\lambda _k(x_{-k})\) and departure rate \(\mu _k\varPhi _k(x_{-k}).\)

SAN representation. Let us describe each class by an automaton. First, transition rates of each automaton are arrival rate and departure rate of the corresponding class. Therefore, these transition rates are functional. Second, if two events of two different classes are not allowed to occur at the same time, transition rates are local. Finally, if the ratio between arrival rate \(\lambda _k(x_{-k})\) and departure rate \(\mu _k\varPhi _k(x_{-k})\) is equal to a constant \(\lambda _k/\mu _k\) for any class \(k\), transition rates are inner proportional. The system is a SAN with local, functional and inner proportional transitions. Thus, Theorem 1 applies and gives us an example of state-dependent multiclass queue with product form solutions w.r.t. classes.

4 Product Form Solution for Untimed Paths

In this section, we refer to a transition as a k-move if it corresponds to an event of automaton \(A_k,\) and we consider an arbitrary starting state \(s=(s_1\ldots s_k\ldots s_N).\) Product form solution for untimed paths is based on the following key result which is a direct consequence of the inner proportional characterisation (Property 1).

Property 2

Conditioning on the event \(E_k^j\) that the first k-move happens at \(jth\) transition, the probability of the event \(Obs(s_k,s^{\prime }_k)\) of observing the move \((s_k,s^{\prime }_k)\) at this first k-move depends neither on the index \(j\) nor on the state of other automata:

$$\begin{aligned} \mathbb P \left(Obs (s_k,s^{\prime }_k)\ |\ E_k^j\right) = \frac{Q_k(s_k,s^{\prime }_k)}{-Q_k(s_k,s_k)}\qquad \forall k,j. \end{aligned}$$
(5)

Assumption.

In the rest of the work, we suppose that automaton \(A_k\) will make a move in the future with probability one if the total outgoing rate of its representative automaton is strictly positive. This assumption states that the system will make a k-move and the first k-move will happen at \(j\)th transition with some finite index \(j\).

Property 3

Conditioning that the total outgoing rate of the representative automaton of \(A_k\) is strictly positive, automaton \(A_k\) will make a move in the future and the probability of observing \((s_k,s^{\prime }_k)\) at the first k-move does not depend on the state of other automata and is given by:

$$\begin{aligned} \mathbb P \left(Obs (s_k,s^{\prime }_k)\ |\ -Q_k(s_k,s_k)>0\right) = \frac{Q_k(s_k,s^{\prime }_k)}{-Q_k(s_k,s_k)}\qquad \forall k. \end{aligned}$$
(6)

In this part, we are interested in checking if state \(s\) satisfies an untimed formula \(\phi \). If the formula corresponds to a set of untimed paths, the work consists in calculating probabilities conditioned on the set of untimed paths starting with \(s\). Let us denote this set by \(U^{(s)}\). Besides, for the representative automaton of \(A_k,\) let \(U_k^{(s_k)}\) be the set of untimed paths starting with \(s_k\).

Definition 1.

For any untimed path \(\sigma = (s^0, s^1, s^2, \ldots )\), its \(k\)-projection is

$$\begin{aligned} proj_k(\sigma ) = (s_k^{i_0}, s_k^{i_1}, s_k^{i_2}, \ldots ),\quad 0=i_0<i_1<i_2<\cdots \end{aligned}$$

such that any two consecutive system states \(s^j, s^{j+1}\) whose \(k\)th components are the same, i.e., \(s_k^j = s_k^{j+1}\), are projected into a unique state \(s_k^j.\)

Thus, a \(k\)-projection of a path is defined such that repeated states are deleted.Consider an arbitrary starting state \(s=(s_1,s_2,\ldots ,s_N)\) and a finite untimed path \(\sigma _k=(s_k,s_k^1,\ldots ,s_k^l)\) of \(A_k\) in isolation. We say that the \(k\)-projection of an untimed path \(\sigma \) starts with \(\sigma _k\) if

$$\begin{aligned} proj_k(\sigma ) = (s_k,s_k^1,\ldots ,s_k^l,\ldots ). \end{aligned}$$

In the rest of the paper, the notation \(proj_k(\sigma )=\sigma _k\) indicates that the \(k\)-projection of \(\sigma \) starts with \(\sigma _k.\) For example, consider \(\sigma _k=(s_k,s^{\prime }_k)\) of length \(1\). Property 3 gives the probability that the \(k\)-projection of \(\sigma \) starts with \((s_k,s^{\prime }_k),\) i.e., automaton \(A_k\) will make a move and the first k-move corresponds to \((s_k,s^{\prime }_k).\)

Theorem 2.

Conditioned on starting states \(s\) and \(s_k\) respectively, the probability of observing an untimed path \(\sigma \) whose \(k\)-projection starts with \(\sigma _k\) is equal to the probability of observing \(\sigma _k\) in the representative automaton of \(A_k{:}\)

$$\begin{aligned} \mathbb P \left(\sigma : proj_k(\sigma )=\sigma _k\ |\ U^{(s)}\right) = \mathbb P \left(\sigma _k\ |\ U_k^{(s_k)} \right). \end{aligned}$$
(7)

In the following we shall consider sets of untimed paths. We first introduce the notion of path-product over these sets.

Definition 2.

For all \(k=1\ldots N,\) let \(U_k\) be a set of untimed paths \(\sigma _k\) in \(\mathcal{{S}}_k.\) The path-product of the sets \(U_1\ldots U_N\) is defined by the set of untimed paths \(\sigma \) in \(\mathcal{{S}},\)

$$\begin{aligned} U \equiv \left\{ \sigma : proj_k(\sigma ) = \sigma _k, \sigma _k \in U_k, k=1\ldots N \right\} , \;{\text{ we} \text{ note}}\;U=\odot U_k. \end{aligned}$$

For example, the set of untimed paths starting with state \(s\) is the path-product of the sets of untimed paths starting with state \(s_k\) of automaton \(A_k\) for all \(k=1\ldots N\), that is, \( U^{(s)} = \odot U_k^{(s_k)}.\)

Theorem 3.

Let \(s\) be an arbitrary starting state, \(U_k\) be a set of finite untimed paths starting with \(s_k\) in \(\mathcal{{S}}_k\) for any automaton \(A_k\), and \(U\) be the path-product \(\odot U_k.\) We have the following product form

$$\begin{aligned} \mathbb P \left(\sigma \in U\ |\ U^{(s)}\right) = \prod _{k=1}^N \mathbb P \left(\sigma _k\in U_k\ |\ U_k^{(s_k)}\right). \end{aligned}$$
(8)

Theorem 3 is important as it gives us a compositional method to check any formulae that is equivalent to a path-product of sets of single component untimed paths. In particular, we shall consider global unbounded Until formulae in the sequel.

Single component unbounded Until formulae: One consequence of Theorem 2 is the following result which provides a compositional method to check any single component untimed formula \(\omega _k.\)

Theorem 4.

For any system state \(s=(s_1,\ldots ,s_k,\ldots ,s_N)\) and for any single component untimed formula \(\omega _k\), the satisfaction of \(\omega _k\) by the whole system is equivalent to its satisfaction by component \(k\): \( \;\;\;s \models \omega _k \Longleftrightarrow s_k \models \omega _k.\)

Thus, one may simply check if state \(s_k\) verifies formula \(\omega _k\) for automaton \(A_k\) in isolation instead of working with global state \(s\). For example, one may remove all functional interactions and only needs to pay attention to the corresponding isolated chain (or isolated class) in the model of generalised competing Markov chains (or multiclass queue with proportional state-dependent rates respectively).

Global unbounded Until formulae: Let \(U^{(\phi \mathcal U \psi )}\) be the set of all untimed paths \(\sigma \) that satisfy the Until formula \((\phi ~\mathcal U ~\psi )\). The probability that \(s\) satisfies \((\phi ~\mathcal U ~\psi )\) is the following probability:

$$\begin{aligned} \mathbb P \left(\sigma \in U^{(\phi \mathcal U \psi )}\ |\ U^{(s)}\right) = \mathbb P \left(\sigma \in U^{(s)} \cap U^{(\phi \mathcal U \psi )}\ |\ U^{(s)}\right). \end{aligned}$$

Theorem 5.

If \(U^{(s)} \cap U^{(\phi \mathcal U \psi )}\) is a path-product of the form

$$\begin{aligned} U^{(s)} \cap U^{(\phi \mathcal U \psi )}=\odot U_k \end{aligned}$$
(9)

where \(U_k\) is some set of finite untimed paths \(\sigma _k\) of automaton \(A_k\) in isolation for all \(k\), the probability that \(s\) satisfies the formula \(\phi ~\mathcal U ~\psi \) has the following product form

$$\begin{aligned} \mathbb P \left(s \models \phi ~\mathcal U ~\psi \right) = \prod _{k=1}^N \mathbb P \left(\sigma _k\in U_k|U_k^{(s_k)}\right). \end{aligned}$$
(10)

This is a direct consequence of Theorem 3 applied to the set \(U = U^{(s)} \cap U^{(\phi \mathcal U \psi )}.\) The idea of this result is to decompose the Until formula probability into separated components. However condition (9) seems to be sophisticated. Let us illustrate it by considering a concrete Until formula in the following.

Application of the compositional approach: Consider the multiclass queue described in Example 2 with batch Poisson arrivals [9]: For each class, arrivals of batches follow a Poisson process, where the batch size is a positive integer random variable. The Poisson parameter and the random variable for the batch size are functional, i.e., may depend on the state of all other classes.Suppose that arrival rates, batch sizes, departure rates depend on the system state such that inner proportional property holds : \(Q_k^s = \alpha _k(s_{-k}) Q_k\quad \forall k. \) With this extension, the SAN remains local, functional and inner proportional.

In a multiclass queue, we are often interested in the number of customers of each class. The logic formulae are to compare this number of customers to a threshold or a composition of these formulae. For each class \(k\), let \(M_k\) be a threshold. We have a failure (overload) for class \(k\) if its number of customers reaches \(M_k\). Whenever this happens the class stays at state \(M_k\) forever by convention, that is, \( Q_k(M_k,s_k) = 0 \;\;\forall s_k\ne M_k. \) On the contrary, the system functions properly if there exists a class \(k\) such as its number of customers does not exceed a threshold \(m_k\). We are interested in verifying the Until formula \((\phi ~\mathcal U ~\psi )\) where

$$\begin{aligned} \left\{ \begin{array}{ll} \phi =\phi _1\vee \cdots \vee \phi _N,&\phi _k=\{x_k\le m_k\}\\ \psi =\psi _1\wedge \cdots \wedge \psi _N,&\psi _k=\{x_k\ge M_k\}. \end{array}\right. \end{aligned}$$
(11)

Condition \(\psi \) means failure of all classes, on the contrary, condition \(\phi \) means that the system functions with at least one class. Let us remark that this Until formula is different from the steady-state probability of being in \(\psi \)-states, we consider indeed the probability to reach \(\psi \)-states passing through \(\phi \)-states.

Consider the probability \(\mathbb P (s\models \phi ~\mathcal U ~\psi )\) for an arbitrary state \(s\). In order to use the above compositional approach, we shall determine the corresponding sets \(U^{(s)}\), \(U^{(\phi \mathcal U \psi )}\) and their intersection. First of all, \(U^{(s)}\) is composed of untimed paths that begin with \(s\). This set is simply the path-product of sets \(U^{(s_k)}_k\) of untimed paths that begin with \(s_k\) for each component \(k\), i.e., \( U^{(s)} = \odot U^{(s_k)}_k. \) Second, \(U^{(\phi \mathcal U \psi )}\) is composed of finite untimed paths that satisfy the Until formula \((\phi ~\mathcal U ~\psi )\). Lastly, the intersection of the two sets is given by the following set of finite untimed paths \( U = \left\{ \sigma : \sigma \ starts\ with\ s, \sigma \models \phi ~\mathcal U ~\psi \right\} . \) Replacing \((\phi ~\mathcal U ~\psi )\) by its definition described by Eq. (11), we obtain \( U=\left\{ \sigma : proj_k(\sigma ) = \sigma _k, \sigma _k \ starts\ with\ s_k,\right. \left.\sigma _k\models \phi _k ~\mathcal U \right. \left. ~\psi _k, k=1\ldots N\right\} = \odot U_k, \) where \( U_k = \left\{ \sigma _k: \sigma _k\ starts\ with\ s_k, \sigma _k\models \phi _k ~\mathcal U ~\psi _k\right\} \). As a result, Theorem 5 can be applied and the probability that \(s\) satisfies \((\phi ~\mathcal U ~\psi )\) is given by

$$\begin{aligned} \prod _{k=1}^N \mathbb P \left(\sigma _k\in U_k\ |\ U_k^{(s_k)}\right) = \prod _{k=1}^N \mathbb P \left(s_k\models \phi _k ~\mathcal U ~\psi _k\right). \end{aligned}$$

In this example, the global Until formula can be decomposed into single component Until formulae. Instead of calculating the probability that some starting state satisfies a global Until formula, one only needs to calculate the product of corresponding single component probabilities.

5 Conclusion

In this paper we prove the product form solutions for the steady-state distribution of a class of SANs which generalises competing Markov chains. We perform the verification of the untimed Until and the steady-state formulae for this class of models through the product form solutions. In the last years, the common points for the performance evaluation and the quantitative model checking have been emphasised by many authors. Product form solutions have been largely used in performance evaluation and we think that it would be interesting to look for classes of models that can be efficiently model checked by means of product form solutions.