Model checking data-independent systems with arrays. - Tom C. Newcomb (2003)