摘要: We present a partial-order reduction technique for local model chee~ ng of hlerarchJca] networks of labeled transition systems in the weak modal mu-calculus. We have implemented our technique in the Concurrency Factory specification and verification environment; experimental results show that partial-order reduction can be highly effective in combating state explosion in modal mu-calculus model checking.