### Recipes for state space reduction

```Recipes for State Space Reduction
Arend Rensink, University of Twente
Dutch Model Checking Day, May 2014
Example (believe it or not): Dining Philosophers
 Start configuration
First grab
left fork
Then grab
right fork
First grab
right fork
Then grab
left fork
Demo
Release
both forks
Recipes for State Space Reduction
9 May 2014
2
Raise atomicity level: Grab both forks
 Suppose we’re not interested in deadlock or starvation
 E.g., study average philosopher load under assumption of liveness
 Essentially, we want to change the grain of atomicity
 Define transactions on top of existing transition system:
 recipe leftThenRight() { grab1left; grab2right; }
recipe rightThenLeft() { grab1right; grab2left; }
or even
 recipe grabBoth() {
choice { grab1left; grab2right; }
or { grab1right; grab2left; }
}
 Intuition
 Abstracted system has single (recipe-labelled) transition
(only) where original system has terminating trace of recipe
Demo
Recipes for State Space Reduction
9 May 2014
3
 Transition systems can grow very large
 Too expensive to generate (time/memory)
 Too large to analyse
 Countermeasures
 State space reduction (partial order, symmetry, …)
 Abstraction (collapsing similar states)
 Coarse-grained atomicity (doing more in one step)
 Context: graph transformation as a modelling formalism
 Transformation steps reflect the dynamics of a system
 GTSs analysed e.g., through model checking
Recipes for State Space Reduction
9 May 2014
4
Recipe semantics
 Example: recipe c() { a; b; }
b
a
c
d
c
a
a
b
b
d
c
b
c
a
a
b
d
c
b
 Challenging cases:
 Refusal behaviour: recipe c() { try a1;b1 else a2; b2; }
 Looping behaviour: recipe c() { alap { a1;b1 } }
 Exploration strategy:
 Local DFS within recipe body
Recipes for State Space Reduction
9 May 2014
5
Message
What are recipes good for?
 State space reduction

 Coarse-grained transitions
 Useful when state space used for further analysis
 Performance gain

 Quantified rules are evaluated faster
Contribution
 Atomicity through composition (on top of existing LTS)
 Also unbounded behaviour
 Compare: action refinement
 Combination with refusals (try, as-long-as-possible)
Recipes for State Space Reduction
9 May 2014
6
```