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.

figure a

1 Introduction

Automata-theoretic approach [VW86] is a key technique for verification and synthesis of systems with linear-time specifications, such as formulae of linear temporal logic (LTL) [Pnu77]. It proceeds in two steps: first, the formula is translated into a corresponding automaton; second, the product of the system and the automaton is further analyzed. The size of the automaton is important as it directly affects the size of the product and thus largely also the analysis time, particularly for deterministic automata and probabilistic model checking in a very direct proportion. For verification of non-deterministic systems, mostly non-deterministic Büchi automata (NBA) are used [EH00, SB00, GO01, GL02, BKŘS12, DLLF+16] since they are typically very small and easy to produce.

Probabilistic LTL model checking cannot profit directly from NBA. Even the qualitative question, whether a formula holds with probability 0 or 1, requires automata with at least a restricted form of determinism. The prime example are the limit-deterministic (also called semi-deterministic) Büchi automata (LDBA) [CY88] and the generalized LDBA (LDGBA). However, for the general quantitative questions, where the probability of satisfaction is computed, general limit-determinism is not sufficient. Instead, deterministic Rabin automata (DRA) have been mostly used [KNP11] and recently also deterministic generalized Rabin automata (DGRA) [CGK13]. In principle, all standard types of deterministic automata are applicable here except for deterministic Büchi automata (DBA), which are not as expressive as LTL. However, other types of automata, such as deterministic Muller and deterministic parity automata (DPA) are typically larger than DGRA in terms of acceptance condition or the state space, respectively.Footnote 1 Recently, several approaches with specific LDBA were proved applicable to the quantitative setting [HLS+15, SEJK16] and competitive with DGRA. Besides, model checking MDP against LTL properties involving frequency operators [BDL12] also allows for an automata-theoretic approach, via deterministic generalized Rabin mean-payoff automata (DGRMA) [FKK15].

LTL synthesis can also be solved using the automata-theoretic approach. Although DRA and DGRA transformed into games can be used here, the algorithms for the resulting Rabin games [PP06] are not very efficient in practice. In contrast, DPA may be larger, but in this setting they are the automata of choice due to the good practical performance of parity-game solvers [FL09, ML16, JBB+17].

Fig. 1.
figure 1

LTL translations to different types of automata. Translations implemented in Rabinizer 4 are indicated with a solid line. The traditional approaches are depicted as dotted arrows. The determinization of NBA to DRA is implemented in ltl2dstar [Kle], to LDBA in Seminator [BDK+17] and to (mostly) DPA in spot [DLLF+16].

Full size image

Types of Translations. The translations of LTL to NBA, e.g., [VW86], are typically “semantic” in the sense that each state is given by a set of logical formulae and the language of the state can be captured in terms of semantics of these formulae. In contrast, the determinization of Safra [Saf88] or its improvements [Pit06, Sch09, TD14, FL15] are not “semantic” in the sense that they ignore the structure and produce trees as the new states that, however, lack the logical interpretation. As a result, if we apply Safra’s determinization on semantically created NBA, we obtain DRA that lack the structure and, moreover, are unnecessarily large since the construction cannot utilize the original structure. In contrast, the recent works [KE12, KLG13, EK14, KV15, SEJK16, EKRS17, MS17, KV17] provide “semantic” constructions, often producing smaller automata. Furthermore, various transformations such as degeneralization [KE12], index appearance record [KMWW17] or determinization of limit-deterministic automata [EKRS17] preserve the semantic description, allowing for further optimizations of the resulting automata.

Our Contribution. While all previous versions of Rabinizer [GKE12, KLG13, KK14] featured only the translation LTL\(\rightarrow \)DGRA\(\rightarrow \)DRA, Rabinizer 4 now implements all the translations depicted by the solid arrows in Fig. 1. It improves all these translations, both algorithmically and implementation-wise, and moreover, features the first implementation of the translation of a frequency extension of LTL [FKK15].

Further, in order to utilize the resulting automata for verification, we provide our own distributionFootnote 2 of the PRISM model checker [KNP11], which allows for model checking MDP against LTL using not only DRA and DGRA, but also using LDBA and against frequency LTL using DGRMA. Finally, the tool can turn the produced DPA into parity games between the players with input and output variables. Therefore, when linked to parity-game solvers, Rabinizer 4 can be also used for LTL synthesis.

Rabinizer 4 is freely available at http://rabinizer.model.in.tum.de together with an on-line demo, visualization, usage instructions and examples.

2 Functionality

We recall that the previous version Rabinizer 3 has the following functionality:

  • It translates LTL formulae into equivalent DGRA or DRA.

  • It is linked to PRISM, allowing for probabilistic verification using DGRA (previously PRISM could only use DRA).

2.1 Translations

Rabinizer 4 inputs formulae of LTL and outputs automata in the standard HOA format [BBD+15], which is used, e.g., as the input format in PRISM. Automata in the HOA format can be directly visualized, displaying the “semantic” description of the states. Rabinizer 4 features the following command-line tools for the respective translations depicted as the solid arrows in Fig. 1:

  • ltl2dgra and ltl2dra correspond to the original functionality of Rabinizer 3, i.e., they translate LTL (now with the extended syntax, including all common temporal operators) to DGRA and DRA [EK14], respectively.

  • ltl2ldgba and ltl2ldba translate LTL to LDGBA using the construction of [SEJK16] and to LDBA, respectively. The latter is our modification of the former, which produces smaller automata than chaining the former with the standard degeneralization.

  • ltl2dpa translates LTL to DPA using two modes:

    • The default mode uses the translation to LDBA, followed by a LDBA-to-DPA determinization [EKRS17] specially tailored to LDBA with the “semantic” labelling of states, avoiding additional exponential blow-up of the resulting automaton.

    • The alternative mode uses the translation to DRA, followed by our improvement of the index appearance record of [KMWW17].

  • fltl2dgrma translates the frequency extension of \(\text {LTL}_ {\setminus {\mathbf {G}}{\mathbf {U}}}\), i.e. \(\text {LTL}_ {\setminus {\mathbf {G}}{\mathbf {U}}}\) [KLG13] with \({\mathbf {G}}^{\sim \rho }\) operatorFootnote 3, to DGRMA using the construction of [FKK15].

2.2 Verification and Synthesis

The resulting automata can be used for model checking probabilistic systems and for LTL synthesis. To this end, we provide our own distribution of the probabilistic model checker PRISM as well as a procedure transforming automata into games to be solved.

  • Model checking: PRISM distribution. For model checking Markov chains and Markov decision processes, PRISM [KNP11] uses DRA and recently also more efficient DGRA [CGK13, KK14]. Our distribution, which links Rabinizer, additionally features model checking using the LDBA [SEJK16, SK16] that are created by our ltl2ldba.

    Further, the distribution provides an implementation of frequency \(\text {LTL}_ {\setminus {\mathbf {G}}{\mathbf {U}}}\) model checking, using DGRMA. To the best of our knowledge, there are no other implemented procedures for logics with frequency. Here, techniques of linear programming for multi-dimensional mean-payoff satisfaction [CKK15] and the model-checking procedure of [FKK15] are implemented and applied.

  • Synthesis: Games. The automata-theoretic approach to LTL synthesis requires to transform the LTL formula into a game of the input and output players. We provide this transformer and thus an end-to-end LTL synthesis solution, provided a respective game solver is linked. Since current solutions to Rabin games are not very efficient we implemented a transformation of DPA into parity games and a serialization to the format of PG Solver [FL09]. Due to the explicit serialization, we foresee the main use in quick prototyping.

3 Optimizations, Implementation, and Evaluation

Compared to the theoretical constructions and previous implementations, there are numerous improvements, heuristics, and engineering enhancements. We evaluate the improvements both in terms of the size of the resulting automaton as well as the running time. When comparing with respect to the original Rabinizer functionality, we compare our implementation ltl2dgra to the previous version Rabinizer 3.1, which is already a significantly faster [EKS16] re-implementation of the official release Rabinizer 3 [KK14]. All of the benchmarks have been executed on a host with i7-4700MQ CPU (4x2.4 GHz), running Linux 4.9.0-5-amd64 and the Oracle JRE 9.0.4+11 JVM. Due to the start-up time of JVM, all times below 2 s are denoted by <2 and not specified more precisely. All experiments were given a time-out of 900 s and mem-out of 4GB, denoted by −.

Algorithmic improvements and heuristics for each of the translations:

  • ltl2dgra and ltl2dra. These translations create a master automaton monitoring the satisfaction of the given formula and a dedicated slave automaton for each subformula of the form \({\mathbf {G}}\psi \) [EK14]. We (i) simplify several classes of slaves and (ii) “suspend” (in the spirit of [BBDL+13]) some so that they appear in the final product only in some states. The effect on the size of the state space is illustrated in Table 1 on a nested formula. Further, (iii) the acceptance condition is considered separately for each strongly connected component (SCC) and then combined. On a concrete example of Table 2, the automaton for \(i=8\) has 31 atomic propositions, whereas the number of atomic propositions relevant in each component of the master automaton is constant, which we utilize and thus improve performance on this family both in terms of size and time.

  • ltl2ldba. This translation is based on breakpoints for subformulae of the form \({\mathbf {G}}\psi \). We provide a heuristic that avoids breakpoints when \(\psi \) is a safety or co-safety subformula, see Table 3.

    Besides, we add an option to generate a non-deterministic initial component for the LDBA instead of a deterministic one. Although the LDBA is then no more suitable for quantitative probabilistic model checking, it still is for qualitative model checking. At the same time, it can be much smaller, see Table 4 which shows a significant improvement on the particular formula.

  • ltl2dpa. Both modes inherit the improvements of the respective ltl2ldba and ltl2dgra translations. Further, since complementing DPA is trivial, we can run in parallel both the translation of the input formula and of its negation, returning the smaller of the two results. Finally, we introduce several heuristics to optimize the treatment of safety subformulae of the input formula.

  • dra2dpa. The index appearance record of [KMWW17] keeps track of a permutation (ordering) of Rabin pairs. To do so, all ties between pairs have to be resolved. In our implementation, we keep a pre-order instead, where irrelevant ties are not resolved. Consequently, it cannot happen that an irrelevant tie is resolved in two different ways like in [KMWW17], thus effectively merging such states.

Table 1. Effect of simplifications and suspension for ltl2dgra on the formulae \(\psi _i = {\mathbf {G}}\phi _i\) where \(\phi _1 = a_1, \phi (i) = (a_i {\mathbf {U}}({\mathbf {X}}\phi _{i-1}))\), and \(\psi '_i = {\mathbf {G}}\phi '_i\) where \(\phi '_1 = a_1\), \(\phi '_1 = (\phi '_{i-1} {\mathbf {U}}({\mathbf {X}}^i a_i)\), displaying execution time in seconds/#states.
Full size table
Table 2. Effect of computing acceptance sets per SCC on formulae \(\psi _1 = x_1 \wedge \phi _1\), \(\psi _2 = (x_1 \wedge \phi _1) \vee (\lnot x_1 \wedge \phi _2)\), \(\psi _3 = (x_1 \wedge x_2 \wedge \phi _1) \vee (\lnot x_1 \wedge x_2 \wedge \phi _2) \vee (x_1 \wedge \lnot x_2 \wedge \phi _3)\), ..., where \(\phi _i = {\mathbf {X}}{\mathbf {G}}((a_i {\mathbf {U}}b_i) \vee (c_i {\mathbf {U}}d_i))\), displaying execution time in seconds/#acceptance sets.
Full size table
Table 3. Effect of break-point elimination for ltl2ldba on safety formulae \(s(n, m) = \bigwedge _{i = 1}^n {\mathbf {G}}(a_i \vee {\mathbf {X}}^m b_i)\) and for ltl2ldgba on liveness formulae \(l(n,m) = \bigwedge _{i = 1}^n {\mathbf {G}}{\mathbf {F}}(a_i \wedge {\mathbf {X}}^m b_i)\), displaying #states (#Büchi conditions)
Full size table
Table 4. Effect of non-determinism of the initial component for ltl2ldba on formulae \(f(i) = {\mathbf {F}}(a \wedge {\mathbf {X}}^i {\mathbf {G}}b)\), displaying #states (#Büchi conditions)
Full size table

Implementation. The main performance bottleneck of the older implementations is that explicit data structures for the transition system are not efficient for larger alphabets. To this end, Rabinizer 3.1 provided symbolic (BDD) representation of states and edge labels. On the top, Rabinizer 4 represents the transition function symbolically, too.

Besides, there are further engineering improvements on issues such as storing the acceptance condition only as a local edge labelling, caching, data-structure overheads, SCC-based divide-and-conquer constructions, or the introduction of parallelization for batch inputs.

Average Performance Evaluation. We have already illustrated the improvements on several hand-crafted families of formulae. In Tables 1 and 2 we have even seen the respective running-time speed-ups. As the basis for the overall evaluation of the improvements, we use some established datasets from literature, see [KMS18], altogether two hundred formulae. The results in Table 5 indicate that the performance improved also on average among the more realistic formulae.

Table 5. Comparison of the average performance with the previous version of Rabinizer. The statistics are taken over a set of 200 standard formulae [KMS18] used, e.g., in [BKS13, EKS16], run in a batch mode for both tools to eliminate the effect of the JVM start-up overhead.
Full size table

4 Conclusion

We have presented Rabinizer 4, a tool set to translate LTL to various deterministic automata and to use them in probabilistic model checking and in synthesis. The tool set extends the previous functionality of Rabinizer, improves on previous translations, and also gives the very first implementations of frequency LTL translation as well as model checking. Finally, the tool set is also more user-friendly due to richer input syntax, its connection to PRISM and PG Solver, and the on-line version with direct visualization, which can be found at http://rabinizer.model.in.tum.de.