University of Twente Student Theses

Login

A comparison of state space reduction techniques in SCOOP

Olthuis, Ferry (2013) A comparison of state space reduction techniques in SCOOP.

[img] PDF
814kB
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 con uence 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 e�ect of the reduction techniques used by SCOOP in di�erent 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 �rst 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 di�erences in the e�ect of the reduction techniques on these 3 models. We show that con uence 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 e�ect of con uence 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.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:http://purl.utwente.nl/essays/64447
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page