Journal of shanghai Jiaotong University (Science) ›› 2015, Vol. 20 ›› Issue (2): 185-194.doi: 10.1007/s12204-014-1554-y

Previous Articles     Next Articles

A Logical Characterization for Linear Higher-Order Processes

A Logical Characterization for Linear Higher-Order Processes

XU Xian1*(徐贤), LONG Huan2 (龙环)   

  1. (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)
  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)
  • Published:2015-04-02
  • Contact: XU Xian(徐贤) E-mail:xuxian@ecust.edu.cn

Abstract: 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.

Key words: 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.

关键词: modal logic| bisimulation| linearity| higher-order| process calculi

CLC Number: