Liveness: moved to multithread DFS instead of BFS to limit state explosion and to find in a considerable faster amount of time a counter example (loop or deadlock). Live paths are pruned.