Optimal Time-Bounded Reachability Analysis for Concurrent Systems

In this work we are interested in the probability to reach a certain set of states of a Markov automaton within a given time bound. However, due to the presence of multiple actions in probabilistic states the behaviour of a Markov automaton is not a stochastic process and thus no probability measure can be defined. This issue is resolved by introducing the notion of a scheduler.

A general scheduler (or strategy) \(\pi : Paths ^*\rightarrow \mathrm {Dist}(\text{ Act })\) is a measurable function, s. t. \(\forall \rho \in Paths ^*\) if \(\rho \mathord \downarrow \in PS \) then \(\pi (\rho ) \in \mathrm {Dist}(\text{ Act }(\rho \mathord \downarrow ))\). General schedulers provide a distribution over enabled actions of a probabilistic state given that the path \(\rho \) has been observed from the beginning of the system evolution. We call stationary such a general scheduler \(\pi \) that can be represented as \(\pi : PS \rightarrow \text{ Act }\), i. e. it is non-randomised and depends only on the current state. The set of all general (stationary) schedulers is denoted by \(\varPi _{\mathtt {gen}}\) (\(\varPi _{\mathtt {stat}}\) resp.).

Given a general scheduler \(\pi \), the behaviour of a Markov automaton is a fully defined stochastic process. For the definition of the probability measure on Markov automata we refer to [Hat17].

Let \(s \in S\), \(T \in \mathbb {Q}_{\geqslant 0}\) be a time bound and \(\pi \in \varPi _{\mathtt {gen}}\) be a general scheduler. The (time-bounded) reachability probability (or value) for a scheduler \(\pi \) and state s in \(\mathcal {M}\) is defined as follows:where \(\Diamond ^{\leqslant T}_{s} G= \{s \overset{\alpha _0,t_0}{\longrightarrow } s_1 \overset{\alpha _1,t_1}{\longrightarrow } s_2 \ldots \mid \exists i: s_i \in G\wedge \sum _{j=0}^{i-1} t_j \le T\}\) is the set of paths starting from s and reaching \(G\) before T.

For \(\mathop {\mathrm {opt}}\in \{\sup , \inf \}\), the optimal (time-bounded) reachability probability (or value) of state s in \(\mathcal {M}\) is defined as follows:We denote by ( ) the vector of values ( ) for all \(s \in S\). A general scheduler that achieves optimum for is called optimal, and the one that achieves value \(\mathbf {v}\), s. t. , is \(\varepsilon \)-optimal.

Optimal Schedulers. For the time-bounded reachability problem it is known [RS13] that there exists an optimal scheduler \(\pi \) of the form \(\pi : PS \times \mathbb {R}_{\geqslant 0}\rightarrow \text{ Act }\). This scheduler does not need to know the full history of the system, but only the current probabilistic state it is in and the total time left until time bound. It is deterministic, i. e. not randomised, and additionally, this scheduler is piecewise constant, meaning that there exists a finite partition \(\mathcal {I}({\pi })\) of the time interval [0, T] into intervals \(I_0=[t_0, t_1], I_1=(t_1, t_2], \cdots , I_{k-1}=(t_{k-1}, t_k]\), such that \(t_0=0, t_k=T\) and the value of the scheduler remains constant throughout each interval of the partition, i. e. \(\forall I \in \mathcal {I}({\pi }), \forall t_1,t_2 \in I, \forall s \in PS {}: \pi (s,t_1) = \pi (s,t_2)\). The value of \(\pi \) on an interval \(I\in \mathcal {I}({\pi })\) and \(s\in PS {}\) is denoted by \(\pi (s, I)\), i. e. \(\pi (s, I) = \pi (s,t)\) for any \(t\in I\).

As an example, consider the MA in Fig. 2 and time bound \(T=1\). Here the optimal scheduler for state \(s_1\) chooses the reliable but slow action \(\beta \) if there is enough time, i. e. if at least 0.62 time is left. Otherwise the optimal scheduler switches to a more risky, but faster path via action \(\alpha \).

In the literature this subclass of schedulers is sometimes referred to as total-time positional deterministic, piecewise constant schedulers. From now on we call a scheduler from this subclass simply a scheduler (or strategy) and denote the set of such schedulers with \(\varPi \). An important notion of schedulers is the switching point, the point of time separating two intervals of constant decisions:

Whether the switching points can be computed exactly or not is an open problem. In fact, the theorem of Lindemann-Weierstrass suggests that switching points are non-algebraic numbers, what hints at a negative answer.

In this section we discuss steps 4 and 9, that require computation of the reachability probability according to the system of Equations (1)–(2). Our approach is based on the approximation of the solution. The presence of two types of states, probabilistic and Markovian, demands separate treatment of those. Informally, we will combine two techniques: time-bounded reachability analysis on continuous time Markov chains³ for Markovian states and time-unbounded reachability analysis on discrete time Markov chains⁴ for probabilistic states. Parameters \(w\) and \(\varepsilon _i\) of Algorithm 1 control the error allowed by the approximation. Here \(\varepsilon _i\) bounds the error for the very first instance of time-unbounded reachability in line 4. While \(w\) defines the fraction of the error that can be used by the approximations in subsequent iterations ( and ).

We start with time-unbounded reachability analysis for probabilistic states. Let \(\pi \in \varPi _{\mathtt {stat}}, s,s' \in S\). We defineThis value denotes the probability to reach state \(s'\) starting from state s by performing any number of probabilistic transitions and no Markovian transitions. This system of linear equations can be either solved exactly, e. g. via Gaussian elimination, or approximated (numerical methods). If is under-approximated we denote it by , where \(\epsilon \) is the approximation error. For \(A\subseteq S\) we define , .

For time bound \(0, s\in PS \) the value is the optimal probability to reach any goal state via only probabilistic transitions. We denote it by (step 4). It is a well-known problem on discrete time Markov decision processes [Put94] and can be computed or approximated by policy iteration, linear programming [Put94] or interval value iteration [HM14, QK18, BKL+17]. If the value is approximated up to \(\epsilon \), we denote it by .

The reachability analysis on Markovian states is solved with the well-known uniformisation approach [Jen53]. Informally, Markovian states will be implicitly uniformised: The exit rate for each Markovian state will be equal \({\mathrm {\mathbf {E}}_{\small {\text {max}}}}\) (by adding a self-loop transition), but this will not affect the reachability value.

We will first define the discrete probability to reach the target vector within k Markovian transitions. Let \(\mathbf {x}\in [0,1]^{|S|}\) be a vector of values for each state. For \(k \in \mathbb {N}_{\geqslant 0}, \pi \in \varPi _{\mathtt {stat}}\) we define if \(s \in G\) and otherwise:The value is the weighted sum over all states \(s'\) of the value \(\mathbf {x}_{s'}\) and the probability to reach \(s'\) starting from s within k Markovian transitions. Therefore the counter k decreases only when a Markovian state performs a transition and is not affected by probabilistic transitions. If values are approximated up to precision \(\epsilon \), i. e. is used for probabilistic states instead of in (4), we use the notation .

We denote with the probability mass function of the Poisson distribution with parameter \(\lambda \). For a \(\tau \in \mathbb {R}_{\geqslant 0}\) and , is some natural number satisfying , e. g. [BHHK15], where e is the Euler’s number.

We are now in position to describe a way to compute at line 9 of Algorithm 1. Let be a vector of values computed by the previous iteration of Algorithm 1 for time t. Let be the solution of the system of Equation (1) for time point \(t+\delta \), a stationary scheduler \(\pi : PS \rightarrow \text{ Act }\) and where is used instead of as the boundary condition⁵. The following Lemma shows that can be efficiently approximated up to :

The strategy for the next interval is computed in Step 7 and implicitly in Step 4. The latter has been discussed in Sect. 4.1. We proceed to Step 7.

Here we search for a strategy that remains constant for all time points within interval \((t, t+\delta ]\), for some \(\delta >0\), and introduces only an acceptable error. Analogously to results for continuous time Markov decision processes [Mil68], we prove that derivatives of function at time \(\tau =t\) help finding the strategy \(\pi \) that remains optimal for interval \((t, t+\delta ]\), for some \(\delta >0\). This is rooted in the Taylor expansion of function via the values of . We define setswhere for \(\pi \in \varPi _{\mathtt {stat}}\), \(s\in G: \mathbf {d}^{(0)}_{\pi }(s)=1\), for , for and for \(i\geqslant 1\):The value \(\mathbf {d}^{(i)}_{\pi }(s)\) is the \(i^{\text {th}}\) derivative of at time t for a scheduler \(\pi \).

Thus in order to compute a stationary strategy that is optimal on time-interval \((t, t+\delta ]\), for some \(\delta >0\), one needs to compute at most \(|S|+1\) derivatives of at time t. Procedure \(\textsc {FindStrategy}\) does exactly that. It computes sets \(\mathcal {F}_i\) until for some \(j\in 0..(|S|+1)\) there is only 1 strategy left, i. e. \(|\mathcal {F}_j|=1\). Otherwise it outputs any strategy in \(\mathcal {F}_{|S|+1}\). Similarly to Sect. 4.1, the scheduler that maximises the values can be approximated. This question and other optimisations are discussed in detail in Sect. 4.4.

Given that a strategy \(\pi \) is computed by \(\textsc {FindStrategy}\), we need to know for how long this strategy can be followed before the action has to change for at least one of the states. We consider the behaviour of the system in the time interval [t, T]. Recall the function , defined in Sect. 4.1 (Lemma 2) as the solution of the system of Equation (1) with the boundary condition , for a stationary scheduler \(\pi \). For a probabilistic state s the following holds:Let \(s \in PS , \pi \in \varPi _{\mathtt {stat}}, \alpha \in \text{ Act }(s)\). Consider the following function:This function denotes the reachability value for time bound \(t+\delta \) and a scheduler that is different from \(\pi \). Namely, this is such a scheduler, that all states follow strategy \(\pi \), except for state s, that selects action \(\alpha \) for the very first transition, and afterwards selects action \(\pi (s)\). Between two switching points the strategy \(\pi \) is optimal and therefore the value of is not greater than for all \(s\in PS {}, \alpha \in \text{ Act }(s)\). If for some \(\delta \in [0, T-t], s \in PS , \alpha \in \text{ Act }(s)\) it holds that , then action \(\alpha \) is better for s then \(\pi (s)\), and therefore \(\pi (s)\) is not optimal for s at \(t+\delta \). We show that the next switching point after time point t is such a value \(t+\delta ,\delta \in (0, T-t]\), thatProcedure \(\textsc {FindStep}\) approximates switching points iteratively. It splits the time interval [0, T] into subintervals \([t_1,t_2], \ldots , [t_{n-1}, t_{n}]\) and at each iteration k checks whether (7) holds for some \(\delta \in [t_{k}, t_{k+1}]\). The latter is performed by procedure \(\textsc {CheckInterval}\). If \(\forall \delta \in [t_k, t_{k+1}]\) (7) does not hold, \(\textsc {FindStep}\) repeats by increasing k. Otherwise, it outputs the largest \(\delta \in [t_{k}, t_{k+1}]\) for which (7) does not hold (line 11). This is done by binary search up to distance \(\delta _{\min }\). Later in this section we will show that establishing that (7) does not hold for all \(\delta \in [t_k,t_{k+1}]\) can be efficiently performed by considering only 2 time points of the interval \([t_k,t_{k+1}]\) and a subset of state-action pairs.

Selecting \(t_k\). This step is a heuristic. The correctness of our algorithm does not depend on the choices of \(t_k\), but its runtime is supposed to benefit from it: Obviously, the runtime of \(\textsc {FindStrategy}\) is best given an oracle that produces time points \(t_k\) which are exactly the switching points of the optimal strategy. Any other heuristic is just a guess.

At every iteration k we choose such a time point \(t_k\) that the MA is very likely to perform at most k Markovian transitions within time \(t_k\). “Very likely” here means with probability . For \(k \in \mathbb {N}\) we define as follows: , and for \(k > 1\): .

Searching for switching points within \([t_{k}, t_{k+1}]\). In order to check whether for all \(\delta \in [t_{k}, t_{k+1}]\) we only have to check whether the maximum of function is at most 0 on this interval for all \(s\in PS ,\alpha \in \text{ Act }(s)\). In order to achieve this we work on the approximation of \(\mathbf { diff }(s, \alpha , t+\delta )\) derived from Lemma 2, thus establishing a sufficient condition for the scheduler to remain optimal:Here ( ) denotes an under-approximation of the value ( resp.) up to , defined in Lemma 2. And analogously for . Simple rewriting leads to the following:where . In order to find the supremum of the right-hand side of (9) over all \(\delta \in [a, b]\) we search for extremum of each , separately as a function of \(\delta \). Simple derivative analysis shows that the extremum of these functions is achieved at \(\delta =i/{\mathrm {\mathbf {E}}_{\small {\text {max}}}}\). Truncation of the time interval by \((\left\lfloor t_{k} \cdot {\mathrm {\mathbf {E}}_{\small {\text {max}}}}\right\rfloor +1) /{\mathrm {\mathbf {E}}_{\small {\text {max}}}}\) (step 4, Algorithm 2) ensures that for all \(i=0..k\) the extremum of \(y_i(\delta )\) is attained at either \(\delta =t_{k}\) or \(\delta =t_{k+1}\).

\(\textsc {CheckInterval}\) returns false iff for all \(s \in PS , \alpha \in \text{ Act }\) the right-hand side of (10) is less or equal to 0. Since Lemma 4 over-approximates \(\mathbf { diff }(s, \alpha , t+\delta )\) false positives are inevitable. Namely, it is possible that procedure \(\textsc {CheckInterval}\) suggests that there exists a switching point within \([t_k, t_{k+1}]\), while in reality there is none. This however does not affect correctness of the algorithm and only its running time.

Finding Maximal Transitions. Here we show that there exists a subset of states, such that, if the optimal strategy for these states does not change on an interval, then the optimal strategy for all states does not change on this interval.

In the following we call a pair \((s,\alpha ) \in PS \times \text{ Act }\) a transition. For transitions \((s, \alpha ), (s', \alpha ') \in PS \times \text{ Act }\) we write \((s,\alpha ) \preceq _{k} (s', \alpha ')\) iff \(C_{\pi , \varepsilon _{\text {N}}}(s,\alpha ) \leqslant C_{\pi , \varepsilon _{\text {N}}}(s',\alpha ')\) and \(\forall i=0..k: B^i_{\pi , \varepsilon _{\text {N}}}(s,\alpha ) \leqslant B^i_{\pi , \varepsilon _{\text {N}}}(s',\alpha ')\). We say that a transition \((s,\alpha )\) is maximal if there exists no other transition \((s',\alpha ')\) that satisfies the following: \((s,\alpha )\preceq _{k} (s',\alpha ')\) and at least one of the following conditions hold: \(C_{\pi , \varepsilon _{\text {N}}}(s,\alpha ) < C_{\pi , \varepsilon _{\text {N}}}(s',\alpha ')\) or \(\exists i=0..k: B^i_{\pi , \varepsilon _{\text {N}}}(s,\alpha ) < B^i_{\pi , \varepsilon _{\text {N}}}(s',\alpha ')\). The set of all maximal transitions is denoted with \(\mathcal {T}_\mathrm {max}(k)\).

We prove that if inequality (10) holds for all transitions from \(\mathcal {T}_\mathrm {max}(k)\), then it holds for all transitions. Thus only transitions from \(\mathcal {T}_\mathrm {max}(k)\) have to be checked by procedure \(\textsc {CheckInterval}\). In our implementation we only compute \(\mathcal {T}_\mathrm {max}(k)\) before the call to \(\textsc {CheckInterval}\) at line 11 of Algorithm 2, and use the set \(A= PS \times \text{ Act }\) within the while-loop.

Here we discuss a number of implementation improvements developers should consider when applying our algorithm to large case studies:

Switching points. It may happen that the optimal strategy switches very often on a time interval, while the effect of these frequent switches is negligible. The difference may be so small that the \(\varepsilon \)-optimal strategy actually stays stationary on this interval. In addition, floating-point computations may lead to imprecise results: Values that are 0 in theory might be represented by non-zero float-point numbers, making it seem as if the optimal strategy changed its decision, when in fact it did not. To counteract these issues we can modify \(\textsc {CheckInterval}\) such that it outputs false even if the right-hand side of (10) is positive, as long as it is sufficiently small. The following lemma proves that the error introduced by not switching the decision is acceptable:

Optimal strategy. In some cases computation of the optimal strategy in the way it was described in Sect. 4.2 is computationally expensive, or is not possible at all. For example, if some values \(|\mathbf {d}^{(i)}_{\pi }(s)|\) are larger than the maximal floating point number that a computer can store, or if the computation of \(|S|+1\) derivatives is already too prohibitive for models of large state space, or if the values can only be approximated and not computed precisely. With the help of Lemma 5 and minor modifications to Algorithm 1, the correctness and convergence of Algorithm 1 can be preserved even when the strategy computed by \(\textsc {FindStrategy}\) is not guaranteed to be optimal.

SwitchStep vs FixStep. Figure 3 compares runtimes of SwitchStep and FixStep. For these experiments precision is set to \(10^{-3}\) and the state space size ranges from \(10^2\) to \(10^5\).

This plot represents the general trend observed in many experiments: The algorithm FixStep does not scale well with the size of the problem (state space, precision, time bound). For larger benchmarks it usually required more than 15 minutes. This is likely due to the fact that the discretisation step used by FixStep is very small, which means that the algorithm performs many iterations. In fact Table 1 reports on the size of the discretisation steps for both FixStep and SwitchStep on a few benchmarks. Here the column \(\delta _{\texttt {F}}\) shows the length of the discretisation step of \(\texttt {FixStep} \). As we mentioned in Sect. 3, this step is fixed for the selected values of time bound and precision. Columns \(\min \delta _{\texttt {S}}\), \(\text {avg}\delta _{\texttt {S}}\) and \(\max \delta _{\texttt {S}}\) show minimal, average and maximal steps used by SwitchStep respectively. The average step used by SwitchStep is several orders of magnitude larger than that of FixStep. Therefore SwitchStep performs much less iterations. Even though each iteration takes longer, overall significant decrease in the amount of iterations leads to much smaller total runtime.

SwitchStep vs \(\texttt {Unif}^{+}\). In order to compare SwitchStep with \(\texttt {Unif}^{+}\) we have to restrict ourselves to a subclass of Markov automata in which probabilistic and Markovian states alternate, and probabilistic states have only 1 successor for each action. This is due to the fact that \(\texttt {Unif}^{+}\) is available in IMCA only for this subclass of models.

Figure 4 shows the comparison of running times of SwitchStep and \(\texttt {Unif}^{+}\). For the plot on the left we varied those model parameters that affect state space size, number of non-deterministic actions and maximal exit rate. In the plot on the right the model parameters are fixed, but precision and time bounds used for the experiments are differing. Table 2 shows the parameters of the models used in these experiments. We observe that there are cases in which SwitchStep performs remarkably better than \(\texttt {Unif}^{+}\), and cases of the opposite. Consider the experiments in Fig. 4, right. They show that \(\texttt {Unif}^{+}\) may be highly sensitive to variations of time bounds and precision, while SwitchStep is more robust in this respect. This is due to the fact that the scheduler computed by \(\texttt {Unif}^{+}\) does not have means to observe time precisely and can only guess it. This may be good enough, which is the case on the \(\texttt {ps}\) benchmark. However if it is not, then better precision will require many more computations. Additionally \(\texttt {Unif}^{+}\) does not use discretisation. This means that the increase of the time bound from \(T_1\) to \(T_2\) may significantly increase the overall running time, even if no new switching points appear on the interval \([T_1, T_2]\). SwitchStep does not suffer from these issues due to the fact that it considers schedulers that observe the time precisely and uses the discretisation. Large time intervals that introduce no switching points will likely be handled within one iteration.

Conclusions: We conclude that SwitchStep does not replace all existing algorithms for time bounded reachability. However it does improve the state of the art in many cases and thus occupies its own niche among available solutions.