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

Linear temporal logic (LTL) [30] is a prominent specification language and has been proven useful in industrial practice. The key to efficient LTL model checking is the automata-theoretic approach [38]: first, a given LTL formula is translated into an automaton; second, a product of the system and the automaton is constructed and analysed. Since real systems are huge, it is crucial to construct small automata in order to avoid a large size increase of the product.

LTL is typically translated into non-deterministic Büchi automata (NBA) [2, 8, 10, 11, 14, 15, 17, 18, 36]. However, for probabilistic models such as Markov decision processes (MDP) non-deterministic automata are not applicable [3] and the standard solution is to determinise them using Safra’s construction [22, 29, 32, 33, 37]. This approach is implemented in the most widespread probabilistic model checker PRISM [27]. However, the determinisation step is costly and often increases the size of automata dramatically. Therefore, direct translations of LTL to deterministic automata have been proposed [1, 13, 25, 26], implemented [5, 16, 24], and shown to be more efficient for probabilistic model checking [6]. Nevertheless, despite more sophisticated acceptance conditions, such as generalized Rabin [26], the imposed determinism inevitably increases the size of the automata.

This naturally raises the question whether fully deterministic automata are necessary or whether restricted forms of determinism are sufficient. For instance, in the setting of games where NBA are not applicable either, a weaker notion of determinism called good-for-games automata is sufficient [20]. It has been proven sufficient also for probabilistic model checking, but practically “did not improve on the standard approach” [23]. Further, unambiguous automata can be used [9] for model checking Markov chains, but not for MDPs. Moreover, limit-deterministic Büchi automata (LDBA) [7, 38] can be used for probabilistic model checking MDPs in the qualitative case (deciding whether a property holds with probability 1). This idea has been further explored also in the quantitative setting (computing the probability of satisfaction) and an algorithm constructing products with several (limit-)deterministic automata proposed [19]. Although LDBA cannot in general be used for probabilistic model checking, a recent translation [35] of LTL produces LDBA, which can be used in the standard algorithm based on the construction of a single product. It also discusses the subclass of LDBA that can be used for this task. Note that there is also an exponentially better translation [21] (based on [25]) of a fragment of LTL called LTL\(_{\setminus {\mathbf {G}}\mathbf {U}}\) into LDBA and that there is also an efficient complementation procedure for LDBA [4].

In this paper, we provide the first implementation of the probabilistic model checking procedure proposed in [35] based on LDBA. Apart from smaller sizes of LDBA, another advantage of the Büchi acceptance condition is a faster analysis of maximal end components (MECs), compared to the standard repetitive re-computation for each Rabin pair. We also present several crucial optimizations, which make our implementation outperform other approaches on many formulas. We illustrate this on experimental results. The tool as well as the explanation of its name can be found on https://www7.in.tum.de/~sickert/projects/mochiba/.

2 Overview of the Algorithm

In order to present our implementation and optimizations, we have to sketch how an MDP \(\mathcal M\) is checked against an LTL formula \(\varphi \) by the algorithm of [35]. First, \(\varphi \) is translated into an LDBA \(\mathcal A(\varphi )\). Second, \(\mathcal M\) is checked against \(\mathcal A(\varphi )\) using a straightforward extension of the standard algorithm.

LDBA Construction. An LDBA is a (possibly generalised) Büchi automaton partitioned into an initial and an accepting part, where the initial part contains no accepting transitions and the accepting part is deterministic. Moreover, the construction of [35] produces LDBA with the initial part deterministic except for \(\varepsilon \)-transitions into the accepting part.

Fig. 1.
figure 1

LDBA \(\mathcal {A}(\varphi )\) with the initial part on the left and the accepting on the right.

Full size image

We illustrate the translation on \(\varphi = a \wedge {\mathbf {X}}({\mathbf {F}}{\mathbf {G}}a \vee {\mathbf {F}}{\mathbf {G}}b)\). Each state in the initial part is labeled with a formula. The words accepted from a state are exactly those satisfying the formula. Observe that \({\mathbf {F}}{\mathbf {G}}a\vee {\mathbf {F}}{\mathbf {G}}b\) holds iff eventually we reach a point where \({\mathbf {G}}a\) holds or \({\mathbf {G}}b\) holds. We non-deterministically guess this point and take the \(\varepsilon \)-transition to the accepting part, where we check the guess.

For this formula spot (2.0) produces a deterministic Rabin automaton with 4 states, too, but adding two more disjuncts \({\mathbf {F}}{\mathbf {G}}c\) and \({\mathbf {F}}{\mathbf {G}}d\) increases the size to 26 states. In contrast, our LDBA requires only two extra states.

Fig. 2.
figure 2

An MDP \(\mathcal M\).

Full size image

Product Construction and Analysis. We proceed according to the standard algorithm:

  1. 1.

    Construct the product \(\mathcal {P}=\mathcal M\times \mathcal A(\varphi )\).

  2. 2.

    Compute maximal end-components (MECs) of \(\mathcal {P}\).

  3. 3.

    Compute the maximum probability to reach winning MECs. A MEC is winning if it satisfies the acceptance condition of \(\mathcal A(\varphi )\): here, if it contains an accepting transition for each Büchi condition.

Fig. 3.
figure 3

The product \(\mathcal M\times \mathcal A(\varphi )\).

Full size image

The standard product of an MDP and a deterministic automaton defines the transitions (in the usual notation) by \(P(\langle s,q\rangle ,\alpha ,\langle s',q'\rangle )=P(s,\alpha ,s')\) if \(q'=\delta (q, Label (s'))\) and otherwise equals 0. We extend the procedure to handle also non-deterministic \(\varepsilon \)-transitions by additional actions: let \(q_1,\ldots ,q_n\) be the successors of q under \(\varepsilon \), then for each \(i=1,\ldots ,n\) we add a new action called \(\varepsilon _{q_i}\) and define \(P (\langle s,q\rangle ,\varepsilon _{q_i},\langle s,q_i\rangle )=1\) (note that s does not move here).

Figure 3 illustrates the construction by a product of the system of Fig. 2 and the automaton of Fig. 1. A crucial optimization used here is that it is sufficient to take \(\varepsilon \)-transitions only from states in MECs of \(\mathcal M\times \mathcal {N}(\varphi )\) (which are exactly MECs of the product of \(\mathcal M\) and the initial part of \(\mathcal A(\varphi )\)). Hence no \(\varepsilon \)-transitions have to be produced in the initial state here.

3 Implementation and Optimizations

MoChiBA [34] replaces the LTL model-checker and the MEC computation in the explicit-state model-checker of PRISM, while other infrastructure (parsing, model construction, probability computation) are inherited from PRISM. The tool cannot be configured — all optimizations are enabled — and does not need to be installed. It reads a model (given as an MDP, .nm) and a property specification (.pctl) and prints the results to stdout:

./mochiba.sh model.nm properties.pctl

Apart from taking \(\varepsilon \)-transitions only from states in MECs of \(\mathcal M\times \mathcal {N}(\varphi )\) as mentioned above, we implement the following optimizations:

Transition-based acceptance leads to smaller automata, compared to state-based acceptance. Consequently, it is used by many translators, for instance [1, 11, 24]. However, PRISM translates all automata to state-based, thus increasing the size of the product. Our procedure avoids this and constructs and analyses directly the transition-based product.

Generalised Büchi acceptance condition allows for more efficient analysis than (generalised) Rabin, Streett, or parity conditions. Indeed, for the latter conditions expensive re-computations of MECs are necessary to handle different sets to be visited finitely often. In contrast, we compute MECs only once and check whether each set to be visited infinitely often intersects the MEC.

A single trap state is present in the product. Should the product enter any state from which the automaton component can never accept, the exploration of this part stops and redirects the transition to the single trap state.

Primitive data structures such as arrays are used instead of the more flexible Java collections, since they are more memory efficient, as boxing into objects is not necessary.

Sparse bit sets have proven more memory efficient for our approach than plain bit sets with a mapping table.

MEC decomposition is performed locally on disconnected accepting parts (corresponding to different \(\varepsilon \)-transitions). Together with the use of sparse bit sets, MECs are computed faster and using less memory.

4 Experimental Evaluation

We evaluate our novel approach in the setting of [6, 19]: we consider the Pneuli-Zuck randomised mutual exclusion protocol [31] of the PRISM benchmark suite [28] and also the same previously considered formulas (see lines 1–10 of Table 1). Additionally, lines 11–14 consider the deeply nested formulas of [35]. Finally, complementary to the \({\mathbf {G}}{\mathbf {F}}\)-, \({\mathbf {F}}{\mathbf {G}}\)- and fairness-like properties, lines 15–16 include simple reachability properties, which lie in the focus of the traditional methods.

The experiments were performed on a 2.5 GHz Intel Core i7 (I7-4870HQ) and granted 12 GB RAM and 1 h computing time for model checking each property (given the model already in the memory). We denote time-outs and mem-outs by “-”. We compare the following tools

  • MoChiBA (1.0) [34] is our implementation based on the LDBA translation of [35] and the explicit model checker of PRISM.

  • PRISM (4.3) [27] with the symbolic engine, which is the fastest here, and with the following translators:

    • Built-in LTL to deterministic Rabin automaton translation, re-implementing ltl2dstar [22].

    • Rabinizer (3.1) [24] using the Safra-less direct translation into generalised Rabin automata, which are now supported by PRISM.

  • IscasMC (unofficial, unversioned) implements the lazy approach of [19], using SPOT 1.2.6 [12] to translate LTL to non-deterministic Büchi automaton. We used the two fastest configurations as listed in [19]:

    • Multi-breakpoint (BP) construction with the explicit engine.

    • Rabin (R) construction with the explicit engine.

Table 1. Runtime comparison on model checking these properties on the Pneuli-Zuck randomised mutual exclusion protocol [31].
Full size table

5 Conclusion

We have implemented a novel approach for probabilistic LTL model checking using a subclass of non-deterministic Büchi automata. Since the experimental results for the explicit state-space implementation are encouraging, we plan to extend the approach to a symbolic one. Further, a parellelisation of the product construction and MECs analysis, as well as dedicated constructions for the Release-operator or various LTL fragments could lead to further speed ups.