A Logical Characterization for Linear Higher-Order Processes  

作　　者：徐贤 龙环 

机构地区：[1]Department of Computer Science and Technology, East China University of Science and Technology [2]Laboratory of Basic Study In Computing Science, MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems, Department of Computer Science and Engineering,Shanghai Jiaotong University

出　　处：《Journal of Shanghai Jiaotong university(Science)》2015年第2期185-194,共10页上海交通大学学报（英文版）

基　　金：the National Natural Science Foundation of China(Nos.61202023,61261130589 and61173048);the PACE Project(No.12IS02001);the Specialized Research Fund for the Doctoral Program of Higher Edueation of China(No.20120073120031)

摘　　要：Modal logic characterization in a higher-order setting is usually not a trivial task because higher-order process-passing is quite different from first-order name-passing. We study the logical characterization of higherorder processes constrained by linearity. Linearity respects resource-sensitiveness and does not allow processes to duplicate themselves arbitrarily. We provide a modal logic that characterizes linear higher-order processes,particularly the bisimulation called local bisimulation over them. More importantly, the logic has modalities for higher-order actions downscaled to resembling first-order ones in Hennessy-Milner logic, based on a formulation exploiting the linearity of processes.Modal logic characterization in a higher-order setting is usually not a trivial task because higher-order process-passing is quite different from first-order name-passing. We study the logical characterization of higherorder processes constrained by linearity. Linearity respects resource-sensitiveness and does not allow processes to duplicate themselves arbitrarily. We provide a modal logic that characterizes linear higher-order processes,particularly the bisimulation called local bisimulation over them. More importantly, the logic has modalities for higher-order actions downscaled to resembling first-order ones in Hennessy-Milner logic, based on a formulation exploiting the linearity of processes.

关 键 词：modal logic BISIMULATION LINEARITY HIGHER-ORDER process calculi 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]