On Model checking data−independent systems with arrays with whole−array operations - Roscoe, A; Lazic, R; Newcomb, T (Springer LNCS, 2005)