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.
[1] Milner R. Communication and concurrency [M]. New Jersey: Prentice Hall, 1989.
[2] Milner R, Parrow J, Walker D. A calculus of mobile processes [J]. Information and Computation, 1992,100(1): 1-77.
[3] Sangiorgi D, Walker D. The π-calculus: A theory of mobile processes [M]. Cambridge: Cambridge Universtity Press, 2001.
[4] Thomsen B. Calculi for higher order communicating systems [D]. London: Department of Computing, Imperial College, 1990.
[5] Sangiorgi D. Expressing mobility in process algebras:First-order and higher-order paradigms [D]. Edinburgh:School of Informatics, University of Edinburgh,1992.
[6] Xu Xian. On the bisimulation theory and axiomatization of higher-order process calculi [D]. Shanghai:Department of Computer Science and Engineering,Shanghai Jiao Tong University, Shanghai, 2008 (in Chinese).
[7] Lanese I, P′erez J A, Sangiorgi D, et al. On the expressiveness of polyadic and synchronous communication in higher-order process calculi [C]//Proceedings of ICALP 2010. New York: Springer-Verlag, 2010:442–453.
[8] Lanese I, P′erez J A, Sangiorgi D, et al. On the expressiveness and decidability of higher-order process calculi[J]. Information and Computation, 2011,209(2): 198-226.
[9] Giusto C D, P′erez J A, Zavattaro G. On the expressiveness of forwarding in higher-order communication[C]//Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC’09). New York: Springer-Verlag, 2009: 155-169.
[10] Xu X. Distinguishing and relating higher-order and first-order processes by expressiveness [J]. Acta Informatica,2012, 49: 445-484.
[11] Yuan Wen-jie, Ying Shi, Wu Ke-jia, et al. Formal description of the evolving reflective requirements specification with π-calculus [J]. Computer Engineering and Science, 2010, 32(6): 146-154 (in Chinese).
[12] You Tao, Du Cheng-lie, Wang Wei, et al. A new component-based real-time system based on timed high-order(THO) calculus [J]. Journal of Northwestern Polytechnical University, 2009, 27(6): 6-11 (in Chinese).
[13] Li Chang-yun, Li Gan-sheng, He Pin-jie. A formal dynamic architecture description language [J]. Journal of Software, 2006, 17(6): 1349-1359 (in Chinese).
[14] Zhan Nai-jun. On timed high-order calculus and its completeness [J]. Science in China: E Series, 2001,31(1): 71-85 (in Chinese).
[15] Fu Y. Checking equivalence for higher order processes[R]. Shanghai: BASICS, Shanghai Jiao Tong University,2005.
[16] Xu X. On bisimulation theory in linear higher-order π-calculus [J]. Transactions on Petri Nets and Other Models of Concurrency III, 2009, 5800: 244-274.
[17] Sangiorgi D. Bisimulation for higher-order process calculi [J]. Information and Computation, 1996,131(2): 141-178.
[18] Parrow J, Sangiorgi D. Algebraic theories for name-passing calculi [J]. Information and Computation,1995, 120: 174-197.
[19] Sangiorgi D. A theory of bisimulation for π-calculus[J]. Acta Informatica, 1996, 33(1): 69-97.
[20] van Benthem J, van Eijck J, Stebletsova V.Modal logic, transition systems and processes [J]. Journal of Logic and Computation, 1994, 4(5): 811-855.
[21] Henessy M, Milner R. Algebraic laws for nondeterminism and concurrency[J]. Journal of the ACM, 1985,32: 137-161.
[22] Milner R, Parrow J, Walker D. Modal logics for mobile processes [J]. Theoretical Computer Science,1993, 114(1): 149-171.
[23] Stirling C. Modal logics for communicating systems[J]. Theoretical Computer Science, 1987, 49: 311-347.
[24] Cleaveland R, Parrow J, Steffen B. The concurrency workbench: A semantics-based tool for the verification of concurrent systems [J]. ACM Transactions on Programming Lnaguages and Systems, 1993,15(1): 36-72.
[25] Amadio R, Dam M. Reasoning about higher-order processes [C]//Proceedings of TAPSOFT’95. New York: Springer-Verlag, 1995: 202-216.
[26] Thomsen B. Plain CHOCS, a second generation calculus for higher-order processes [J]. Acta Informatica,1993, 30(1): 1-59.
[27] Baldamus M, Dingel J. Modal characterization of weak bisimulation for higher-order processes[C]//Proceedings of TAPSOFT’97. New York:Springer-Verlag, 1997: 285-296.
[28] Koutavas V, Hennessy M. First-order reasoning for higher-order concurrency [J]. Computer Languages,Systems and Structures, 2012, 38(3): 242-277.
[29] Jeffrey A, Rathke J. Contextual equivalence for higher-order π-calculus revisited [J]. Logical Methods in Computer Science, 2005, 1(1): 1-20.
[30] Sangiorgi D, Kobayashi N, Sumii E. Environmental bisimulations for higher-order languages [J]. ACM Transactions on Programming Languages and Systems,2011, 33(1): 1-10.
[31] Caires L, Cardelli L. A spatial logic for concurrency:Part I [J]. Information and Computation, 2003,186(2): 194-235.
[32] Caires L, Cardelli L. A spatial logic for concurrency:Part II [J]. Theoretical Computer Science, 2004,322(3): 517-565.
[33] Cao Z. A spatial logical characterisation of context bisimulation [C]//Proceeding of ASIAN2006. New York: Springer-Verlag, 2006: 232-240.
[34] Cao Z. Modal ZIA, modal refinement relation and logical characterization [C]//Proceedings of SEKE2012.California: World Scientific Publishing Co., 2012: 525-530.
[35] Cao Z. Reducing higher order π-calculus to spatial logics [C]//Proceedings of COMPUTATION TOOLS 2013. Valencia: Xpert Publishing Services, 2013: 44-53.
[36] Lago U D, Martini S, Sangiorgi D. Light logics and higher-order processes [C]//Proceedings of Workshop on Expressiveness in Concurrency 2010 (EXPRESS 2010). Sydney: EPTCS, 2010: 46-60.
[37] Kobayashi N, Yonezawa A. Higher-order concurrent linear logic programming [C]//Proceedings of International Workshop TPPP ’94. New York: Springer-Verlag, 1994: 137-166.
[38] Frauenstein T, Baldamus M, Glas R. Congruence proofs for weak bisimulation on higher-order processes:Results for typed ω-order calculi [R]. Berlin: Berlin University of Technology, Computer Science Department,1996.
[39] Barendregt H P. The lambda calculus: Its syntax and semantics [M]. [s.l.]: North-Holland, 1984.
[40] Barras B, Boutin S, Cornes C, et al. The Coq proof assistant (reference manual) [R]. [s.l.]: The Coq Development team, 2012.
