Read, Write and Copy Dependencies for Symbolic Model Checking

This paper aims at improving symbolic model checking for explicit state modeling languages, e.g.,

Promela

,

Dve

and

mCRL

2. The modular

Pins

architecture of

LTSmin

supports a notion of event locality, by merely indicating for each event on which variables it depends. However, one could distinguish four separate dependencies:

read

,

may-write

,

must-write

and

copy

. In this paper, we introduce these notions in a language-independent manner. In particular, models with arrays need to distinguish overwriting and copying of values.

We also adapt the symbolic model checking algorithms to exploit the refined dependency information. We have implemented refined dependency matrices for

Promela

,

Dve

and

mCRL

2, in order to compare our new algorithms to the original version of

LTSmin

. The results show that the amount of successor computations and memory footprint are greatly reduced. Finally, the optimal variable ordering is also affected by the refined dependencies: We determined experimentally that variables with a read dependency should occur at a higher BDD level than variables with a write dependency.