A Multistep Extending Truncation Method towards Model Construction of Infinite-State Markov Chains

1. Introduction

Continuous Time Markov Chains (CTMCs) have been used in various areas of research as a formalism; so far, the model checking of CTMCs has been a hot research topic in computer science research communities. Some algorithms and implementations have been shown in several papers and tools [1–7]. However, our research aims to the model checking problem of the Infinite-State CTMCs, which means that the states of the CTMCs in our interest can be infinite. The papers [8–11] and the tool INFAMY [7] are with the same interest, which are also our research basis. Due to the explosion of states of CTMCs, our approach is based on a truncated CTMC model, which is determined by the exploration on the fly [9, 10], which means that the depth of model is computed dynamically by the exploration of states.

The truncation process is involved with reachability analysis [9, 10]; that is, the transient probability is computed with the exploration of the model. The transient probability is carried out by uniformization method [10]. Together with the transient analysis when constructing the model, computation is very heavy, so to get a sufficient truncated model to meet the requirement of related Continuous Stochastic Logic (CSL) property or certain precision as fast as possible is our destination. We introduce a multistep extending advanced truncation method to meet this end, and the experimental results show our method is effective.

The main contents of the paper are organized as follows. Section 2 introduces the truncation based reachability analysis; Section 3 introduces an advanced truncation algorithm and do experiments. Section 4 proposes some multistep extending solutions and experiments. Section 5 talks about our result and next job.

2. Truncation Based Reachability Analysis

2.1. Finite Truncations

Let 𝒞 = (S, R, L) be a CTMC, where S is a countable set of states, R : (S × S → ℝ_≥0) is the rate matrix, and L : S → 2^AP is a labeling function.

First, we introduce some paths and probabilistic measures from [9]. A (timed) infinite path is an infinite sequence σ = s₁t₁s₂t₂… satisfying R(s_i, s_i+1) > 0, and t_i ∈ ℝ_≥0 for all i = 1,2, …. For the path σ and i ∈ N, let σ[i] = s_i denote the (i + 1)th state, and let δ(σ, i) = t_i denote the time spent in s_i. For t_i ∈ ℝ_≥0, let σ@t denote σ[i] such that i is the smallest index with $$. For 𝒞, let $$ denote the set of all paths, and let $$ denote the set of all paths starting from s. For state s ∈ S, a probability measure, denoted by $$, on the set $$ can be defined. A finite path is a finite sequence σ = s₁t₁s₂t₂ … s_k for k > 0 satisfying R(s_i, s_i+1) > 0 and t_i ∈ ℝ_≥0 for i = 1,2, …, k − 1. Let len(σ) = k − 1 denote the length of the path, first(σ) = s₁ denote the first state, and last(σ) = s_k denote the last state of the path. Let $$ denote the set of all finite paths. We omit the superscript 𝒞 if it is clear from context.

Next, we introduce the notion of depth. Let S₀ be a finite subset of S with depth 0; that is, d(s) = 0 for s ∈ S₀. For now, one may think of S₀ as being equal to the support of the initial distribution μ. However, S₀ can be an arbitrary finite set. This will allow us not only to deal with the initial distribution, but also to compute truncation depths for nested CSL formulas. The depth of state s corresponds to the minimal distance from the set S₀.

Definition 1. For 𝒞 and S₀ ⊂ S, the depth function d : S → ℕ is defined by $$.

Observe that $$ for all s ∈ S₀. The subscript is omitted if S₀ is clear from the context. Intuitively, d(s) corresponds to the minimal length of any finite path starting from S₀ and ending in s.

We consider a partition of the state space S = ⋃_i∈ℕ S_i, where S_i : = {s ∈ S∣d(s) = i} is the set of states with depth i. We say that the set S_i is the layer with depth i and call its elements layer-i states. Assume that ⊥∈S is a special state not in S and furthermore ⊥ is also an atomic proposition not in AP. For k ∈ ℕ, let S_>k ⊂ S denote the set of states with depth greater than k; that is, S_>k = {s∣d(s) > k}.

Further, we write S_≤k = S∖S_>k. We define the k-truncated CTMC as follows.

Definition 2. Let 𝒞 = (S, R, L) be a CTMC and let S₀ be the layer-zero states. For k ∈ ℕ, we define the k-truncated CTMC of 𝒞 by 𝒞∣_k = (S∣_k, R_k, L_k), where the states are S∣_k = S_≤k ∪ {⊥}. The labeling function L_k : S∣_k → AP ∪ {⊥} is defined by L_k(s) = L(s) if s ∈ S_≤k, and L_k(⊥) = {⊥}. The rate matrix is defined by the following: R_k(s, s^′) equals S(s, s^′) if s, s^′ ∈ S_≤k, equals $$ if s ∈ S_k, s^′ = ⊥, and equals 0 otherwise.

The k-truncation of an infinite CTMC is illustrated in Figure 1. Intuitively, the transition matrix is restricted to the truncated state space S∣_k, and ⊥ is the distinguished absorbing state, which, by construction, is only reachable from states with depth k. In state ⊥ only the atomic proposition ⊥ holds, which indicates that the system is in state ⊥. Since we consider finitely branching CTMCs, not surprisingly, the k-truncated CTMC 𝒞∣_k is always finite. The absorbing state ⊥ has been introduced to abstract S_>k. We assume that ⊥∉Sat(Φ) for any state formula Φ. We consider the probability of reaching the absorbing state ⊥ in the k-truncated CTMC 𝒞∣_k, that is, $$. For mere notational convenience, we extend $$ to states of 𝒞 with depth higher than $$ for all s^′ ∈ S with d(s^′) > k. For a fixed k, we define the forward rate fr_k(s) of a state s ∈ S_≤k within 𝒞∣_k. For s ∈ S_≤k∖S_k, it is the sum of the rates that go into the next layer fr_k(s) = R(s, S_d(s)+1), and, for s ∈ S_k, it is the sum fr_k(s) = R(s, S_>k) of the rates entering states in S_k.

3. An Advanced Truncation Algorithm and Experiments

The truncation process is implemented by extending the states layer by layer from the initial states, and all the new states need to be transient analyzed and then to be extended further no matter how small the probability is. For that the precision of the result is under some certain value, so some states with relatively nearly no contribution to the result can be omitted when extending; thus, an advanced truncation algorithm is introduced. It is different from the finite state projection (FSP) [9, 10] and layered chain and uniform chain method [9, 10]. The algorithm is shown in Algorithm 1.

The algorithm aims to stop the extending of less important (small probability) states and proceed to the extending of much important (large probability) states; the less or more is determined by the state reduction policy; as shown in Figure 2, line 7, $$ and $$. The policy means that the states in the border states set, which has been sorted upward, $$, will be excluded from the extending states set, for the sum of them is just exactly less than the precision. So with this policy, the number of states to be transient analyzed will be smaller to the FSP and forward-layered based model.

We consider the dependability of a fault-tolerant workstation cluster which is directly taken from case studies of [7]. Figure 2 depicts a dependable cluster of workstations. The cluster consists of two subclusters, which, in turn, contain N workstations connected via a central switch. The two switches are connected via a backbone. Each component of the system can break down and is then fixed by a single repair unit responsible for the entire system. Hereby, the quality of service (QoS) constraint minimum requires at least k  (k < N) workstations to be operational, where k = ⌊(3/4)N⌋. Workstations have to be connected via switches. If in each subcluster the number of operational workstations is smaller than k, the backbone is required to be operational to provide the required service. We consider the property.

𝒫 = ?◊[0, t]¬Minimum. This probability means that the QoS drops below minimum quality within t time unit.

For the property, we compare PRISM [6], FSP method and layered method of INFAMY. The results are given in Tables 1, 2, and 3. Because the resulting probabilities are very small in some cases, we use a precision of 10⁻⁶ here, for the computation of the truncation point. Results for INFAMY are given for the layered chain, FSP, and advanced configurations, respectively. The uniform chain configuration is omitted, as it is always dominated by the layered chain configuration. PRISM implements three different engines: a sparse-matrix and two symbolic engines. We used the sparse-matrix engine as it was the fastest one. The results are shown in Tables 1, 2, and 3.

The experiment conditions are shown as follows.

Host Machine: it includes Mac Book, OS: Mac OS X 10.6.8, Processor: 2.2 GHz Intel Core 2 Duo T7500, and Storage: 2 GB 667 MHz DDR3 SDRAM.

Guest Machine: it includes Virtual Machine Software: VirtualBox 4.1.14  r77440 for mac; Virtual OS: Linux ubuntu12.04 LTS 32Bit; Processor: 2.2 GHz Intel Core 2 Duo T7500; Storage: 512 MB

From Tables 1, 2, and 3, we can see that, for t ≤ 20, FSP based INFAMY is faster, but for t ≤ 30, t ≤ 50, INFAMY model checker needs more time; this is because the transient analysis when constructing the model needs more computing. This is also the result of [11]. For the advanced method of the context, as in Tables 1, 2, and 3, comparing advanced with FSP, we can get that, under advanced based method, the depth of model is much deeper, and the states number is smaller; for the time costing, for t ≤ 20, t ≤ 30, the costing is less reduced, but for t ≤ 50, the costing is greater; this result is reasonable, for the exploration policy is essentially undeterministically efficient for different models; for the current case, when t ≤ 50, the current states number is very large, even with the reduction policy, with no contribution for it any more. We need to take other techniques to tackle this situation. Thus, we propose a multistep extending solution. See Section 4.

4. Multistep Extending Solutions and Experiments

The mutistep extending solution aims to reduce the extending of less important (small probability) states and enhance the extending of more important (large probability) states; for the latter states, we can, for example, extend two or more steps per extending, and for the former states, we can, for example, extend one step per extending, as we know that transient probabilities will be computed once again before the states were added to the border states, so, if we extend two or more steps, transient analysis at the intermediate states will be omitted; thus, time on the model construction will be reduced; then we can make the model much faster to converge to the absorbing state.

The experiment results are as shown in Table 4. From Table 4, we can see that current solution D performs better on this case.

5. Conclusion

The multistep extending advanced truncation method can improve the efficiency of model construction of Infinite-State CTMCs; this is because the transient probabilities of states which have been jumped have not been computed, so to some extent this method is effective; however, which solution performs better needs to be experimented; there is no general solution that fits well for all cases. The efficiency is determined by the iterations when computing the transient probability. Less iteration is more efficient. However, this approach is essentially a linear approach to improve the efficiency; when the outsider state gets explosion, this approach will be less effective; just as in our case study, this approach can be used effectively to improve the model checking efficiency at a relatively small time bound t. For future work, we need to consider other techniques to tackle the state explosion problem on model checking of CTMCs. And other works like [12–15] can also be considered.

Conflict of Interests

The authors declare that there is no conflict of interests regarding the publication of this paper.