1. A method performed by a computer of performing a sound transaction-based reduction on a state space to facilitate model checking for a concurrent computer program having plural threads, the method comprising: exploring an execution path for a first thread of the plural threads in the concurrent computer program; delaying execution of a second thread of the plural threads in the concurrent computer program; determining a commit point for the first thread; determining whether a path from the first thread to the delayed second thread exists after the commit point; if no path from the first thread to the delayed second thread exists after the commit point, scheduling the delayed second thread for execution; and if a path from the first thread to the delayed second thread exists after the commit point, omitting scheduling of the delayed second thread without performing cycle detection in the execution path for the first thread.