科研之友
微信
新浪微博
Facebook
分享链接
摘要
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.
