Model checking is a widely used method for software and hardware validation. It shows either the correctness of a program or produces a counter-example, by performing a search on the whole state space. Therefore model checking is very sensitive to the size of the state space. The number of states may grow exponentially with the number of processes in a parallel composition. Especially for systems that communicate asynchronously, the queues contribute to a combinatorial explosion of the state space.
In this work we use constraints to represent states in enumerative model checking. This reduces the state space by merging states that differ only in the data in the queue. In contrast to abstraction, this method is exact, i.e., only the truly reachable states are considered. The representation with constraints has advantages for systems whose behavior is influenced by random data, such as open systems. To substantiate its benefits, is is compared to the standard representation of states with concrete values for variables and with state-of-the-art model checkers.