In this paper, bounded model checking of asynchronous concurrentsystems is introduced as a promising application area for answer setprogramming. As the model of asynchronous systems a generalisationof communicating automata, 1-safe Petri nets, are used. It is shownhow a 1-safe Petri net and a requirement on the behaviour of the netcan be translated into a logic program such that the bounded modelchecking problem for the net can be solved by computing stablemodels of the corresponding program. The use of the stable modelsemantics leads to compact encodings of bounded reachability anddeadlock detection tasks as well as the more general problem ofbounded model checking of linear temporal logic. Correctness proofsof the devised translations are given, and some experimental resultsusing the translation and the Smodels system are presented.