On decidability and model checking for a first order modal logic for value-passing processes  

作　　者：薛锐 林惠民 

机构地区：[1]Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences

出　　处：《Science in China(Series F)》2003年第1期45-59,共15页中国科学（F辑英文版）

基　　金：This work was partially supported by the National Natural Science Foundationof China (Grant No. 69833020); the National High Technology Development Program of China (Grant No. 2002AA144050);the National Grand Fundamental Research 973 Program of China

摘　　要：A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named HML(FO), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic HML(FO2) of HML(FO) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to HML(FO2) is obtained.

关 键 词：first order modal logic DECIDABILITY model checking value-passing processes. 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]