Good-for-MDPs Automata
319
5 Evaluation
5.1 Size of General B ¨
uchi Automata for Probabilistic Model Checking
As discussed, automata that simulate slim automata or SLDBAs are good for MDPs.
This fact can be used to allow B¨ uchi automata produced from general-purpose tools
such as SPOT’s [8] ltl2tgba rather than using specialized automata types. Automata
produced by such tools are often smaller because such general-purpose tools are highly
optimized and not restricted to producing slim or limit deterministic automata. Thus,
one produces an arbitrary B¨ uchi automaton using any available method, then transforms
this automaton into a slim or limit deterministic automaton, and finally checks whether
the original automaton simulates the generated one.
We have evaluated this idea on random LTL formulas produced by SPOT’s tool
randltl. We have set the tree size, which influences the size of the formulas, to 50,
and have produced 1000 formulas with 4 atomic propositions each. We left the other
values to their defaults. We have then used SPOT’s ltl2tgba (version 2.7) to turn these
formulas into non-generalized B¨ uchi automata using default options. Finally, for each
automaton, we have used our tool to check whether the automaton simulates a limit
deterministic automaton that we produce from this automaton. For comparison, we have
also used Owl’s [29] tool ltl2ldba (version 19.06.03) to compute limit deterministic nongeneralized Buchi automata. We have also used the option of this tool to compute B¨ uchi
automata with a nondeterministic initial part. We used 10 minute timeouts.
Of these 1000 formulas, 315 can be transformed to deterministic B¨ uchi automata.
For an additional 103 other automata generated, standard simulation sufficed to show
that they are GFM. For a further 11 of them, the simplest AEC simulation (the spoiler
chooses an accepting transition to occur infinitely often) sufficed, and another 1 could
be classed GFM by allowing the duplicator to update the transition. 501 automata turned
out to be nonsimulatable and for 69 we did not get a decision due to a timeout.
For the LTL formulas for which ltl2tgba could not produce deterministic automata,
but for which simulation could be shown, the number of states in the generated automata
was often lower than the number of states in the automata produced by Owl’s tools. On
average, the number of states per automaton was ≈15.21 for SPOT’s ltl2tgba; while for
Owl’s ltl2ldba it was ≈46.35. The extended version of this paper [13] contains more
details about the evaluation.
1 2 3 4 5
0.6
0.8
1
Fig. 4. Deciles ratio ltl2tgba
/semi-deterministic automata
Let us consider the ratio between the size of automata
produced by ltl2tgba and the size of semi-deterministic
automata produced by Owl. The average of this number
for all automata that are not deterministic and that can
be simulated in some way is ≈ 1.0335. This means that
on average, for these automata, the semi-deterministic
automata are slightly smaller. If we take a look at the
first 5 deciles depicted in Fig. 4, we see that there is a
large number of formulas for which ltl2tgba and Owl
produce automata of the same size. For around 24.3478% of the cases, automata by
SPOT are smaller than those produced by Owl (ratio < 1).
319
5 Evaluation
5.1 Size of General B ¨
uchi Automata for Probabilistic Model Checking
As discussed, automata that simulate slim automata or SLDBAs are good for MDPs.
This fact can be used to allow B¨ uchi automata produced from general-purpose tools
such as SPOT’s [8] ltl2tgba rather than using specialized automata types. Automata
produced by such tools are often smaller because such general-purpose tools are highly
optimized and not restricted to producing slim or limit deterministic automata. Thus,
one produces an arbitrary B¨ uchi automaton using any available method, then transforms
this automaton into a slim or limit deterministic automaton, and finally checks whether
the original automaton simulates the generated one.
We have evaluated this idea on random LTL formulas produced by SPOT’s tool
randltl. We have set the tree size, which influences the size of the formulas, to 50,
and have produced 1000 formulas with 4 atomic propositions each. We left the other
values to their defaults. We have then used SPOT’s ltl2tgba (version 2.7) to turn these
formulas into non-generalized B¨ uchi automata using default options. Finally, for each
automaton, we have used our tool to check whether the automaton simulates a limit
deterministic automaton that we produce from this automaton. For comparison, we have
also used Owl’s [29] tool ltl2ldba (version 19.06.03) to compute limit deterministic nongeneralized Buchi automata. We have also used the option of this tool to compute B¨ uchi
automata with a nondeterministic initial part. We used 10 minute timeouts.
Of these 1000 formulas, 315 can be transformed to deterministic B¨ uchi automata.
For an additional 103 other automata generated, standard simulation sufficed to show
that they are GFM. For a further 11 of them, the simplest AEC simulation (the spoiler
chooses an accepting transition to occur infinitely often) sufficed, and another 1 could
be classed GFM by allowing the duplicator to update the transition. 501 automata turned
out to be nonsimulatable and for 69 we did not get a decision due to a timeout.
For the LTL formulas for which ltl2tgba could not produce deterministic automata,
but for which simulation could be shown, the number of states in the generated automata
was often lower than the number of states in the automata produced by Owl’s tools. On
average, the number of states per automaton was ≈15.21 for SPOT’s ltl2tgba; while for
Owl’s ltl2ldba it was ≈46.35. The extended version of this paper [13] contains more
details about the evaluation.
1 2 3 4 5
0.6
0.8
1
Fig. 4. Deciles ratio ltl2tgba
/semi-deterministic automata
Let us consider the ratio between the size of automata
produced by ltl2tgba and the size of semi-deterministic
automata produced by Owl. The average of this number
for all automata that are not deterministic and that can
be simulated in some way is ≈ 1.0335. This means that
on average, for these automata, the semi-deterministic
automata are slightly smaller. If we take a look at the
first 5 deciles depicted in Fig. 4, we see that there is a
large number of formulas for which ltl2tgba and Owl
produce automata of the same size. For around 24.3478% of the cases, automata by
SPOT are smaller than those produced by Owl (ratio < 1).