关键词: 通信顺序进程，回答集编程，I_ TI_/ChI.

Abstract: Traditionally,the verification of properties of Communicating Sequential Processes (CSP) is carried out on three different levels of models, which increases the complexity and difficulty of developing verification tools. At the same time,mainstream tools for verifying concurrent systems cannot verify multiple properties at one run of the tools, which decreases the verification efficiency of the tools. To deal with the problems, this paper proposed an ASP-based u- nified framework for verifying concurrent systems described by CSP. The method first transforms CSPs into the An- saver Set Program, and then transforms the execution rules for concurrent CSP processes and the properties in the form of LTL/CTL formulae into the rules of ASP. At last, the properties can be verified by a computation of the answer sets of the resulting ASP program. It is shown that the ASP based method for verifying CSP concurrent system is easy to implement,is able to verify multiple LTL/CTL formulae at one execution of the verification software,and at the same time achieves acceptable time efficiency.

Key words: Communicating sequential processes,Answer set program,LTL/CTL