Publication at Faculty of Mathematics and Physics |
2007
Abstract
In model checking, the number of states of a model tends to grow exponentially with the size of the model's description, leading to unacceptable space and time requirements. Focusing on generalized interaction protocols (Interfering Automata), we present a method of substitution of groups of states by a single state (representative) during the verification.
As the number of representatives is significantly smaller than the size of the whole state space, our method pushes the limits of practical verification. Our approach is focused on parallel and distributed model checking.