A Logical Characterization for Linear Higher-Order Processes

作     者：徐贤 龙环 

作者机构：Department of Computer Science and Technology East China University of Science and Technology Laboratory of Basic Study In Computing Science MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems Department of Computer Science and EngineeringShanghai Jiaotong University 

出 版 物：《Journal of Shanghai Jiaotong university(Science)》 (上海交通大学学报（英文版）)

年 卷 期：2015年第20卷第2期

页      面：185-194页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：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 bisimulation linearity higher-order process calculi 

摘      要：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.