Model checking is a mainstream method for formal verification of communicating sequential processes (CSP). Existing CSP model checkers are based on operational semantics, which need to translate processes into a label transition system, and to extract the semantic model based on the system. The conversion process is complex. Moreover, in most CSP model checkers, the properties to be verified are described by CSP, which is helpful for refinement checking, but at the same time leads to limited description power and weak generality. To address these issues, a new denotational semantic model of CSP, critical-trace model, is proposed and proved to be reliable for model checking CSP. Based on this model, a framework for model checking CSP is established to allow critical-trace model to be constructed inductively from the traces of its components, and properties to be specified by linear temporal logic (LTL), a universal property specification language. In addition, automatic mechanisms for generating critical-trace model and verifying LTL formulas are implemented with answer set programming (ASP). Finally, the two mechanisms are integrated into a CSP model checker T_ASP. Compared with the similar systems developed previously, experimental results indicate a higher ability of the proposed system to describe CSP processes and higher verification accuracy. Furthermore, T_ASP checks multiple properties in one execution of the system. When a property is not satisfied, the system also returns counterexamples for the property.