Validating the correctness of systems by generating the corresponding state space (SSp) is a common method limited by the possible exponential growth of its size, known as the SSp explosion problem. Probabilistic methods focus on analyzing just a fraction of the SSp by means of partial exploration, but the probability of omitting states is greater than zero, sometimes incorrect evaluations are bound to happen and conclusiveness is not achievable all the time.
展开▼
