Abstract:Asynchronous programs use asynchronous non-blocking calls to achieve program concurrency, are widely used in parallel and distributed systems. The complexity of verifying asynchronous programs is very high, no matter safety or liveness . This paper proposes a program model of asynchronous programs, and defines two problems on asynchronous programs:the-equivlence problem and reachability problem. By reducing the 3-CNF-SAT to these two problems, and then reducing them to the reachablity problem of communication-free Petri net, we prove that the two problems are both NP-complete. The case shows that these two problems can solve a series of program verification problems on asynchronous programs.