文献类型：期刊文献

中文题名：A Logical Characterization for Linear Higher-Order Processes

英文题名：A logical characterization for linear higher-order processes

作者：Xu, Xian[1]; Long, Huan[2]

机构：[1] Department of Computer Science and Technology, East China University of Science and Technology, Shanghai, 200237, China; [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, Shanghai, 200240, China

年份：2015

卷号：20

期号：2

起止页码：185

中文期刊名：Journal of Shanghai Jiaotong university(Science)

外文期刊名：Journal of Shanghai Jiaotong University (Science)

收录：EI(收录号：20144200096858);Scopus

基金：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

外文关键词：Computer circuits

摘要：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 higher-order 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. ? 2014, Shanghai Jiaotong University and Springer-Verlag Berlin Heidelberg.