Abstract

In quantitative model checking we are concerned with verifying both quantitative and qualitative properties over models. Markov Automata are what we use to model these systems. In these transition systems nondeterminism, probabilistic behaviour and behaviour over time can all be modelled. SCOOP is a tool that uses several techniques, including confluence reduction and dead variable reduction, to reduce the state space of a Markov Automaton.

In this work, we present a research in which we compare the effect of the reduction techniques used by SCOOP in different case studies. This is relevant in two aspects. For potential users of SCOOP we provide concrete proof that SCOOP and its reduction techniques can be a solution to their problems. It also gives more insights in why SCOOP does not work in some situations and provide directions to where the implementation of SCOOP could be improved.

We modelled a set of case studies in MAPA (the process algebra used by SCOOP), in order to show the strengths and weaknesses in SCOOP. The first case study is a Gossip Protocol. This is a means by which computer systems can communicate in a way similar to how gossip spreads through a community. In the second game we model a trade market, originating from an electroinic strategy game called Gazillionaire. The third and last case study describes a means by which a group of robots comes to consensus of the best out of two options. They do so in a way similar to how ants seek the shortest path to a food source.

We show that there are huge differences in the effect of the reduction techniques on these 3 models. We show that confluence reduction has no impact at all on the gossip model and that it only slightly decreases the state space size of the other three models. We could come nowhere near the numbers shown in previous case studies. This is partly due to the density of relevant communication and rates in the model. We also show that if we extract the core from the model and show that if the basic sequence of actions forming gets large, this negatively impacts the effect of confluence reduction. For dead variable reduction we show that this only works for the gossip model (from our 3 models) because this is a phased type model.

Additional Resources

1. The paper