A Logical Characterization for Linear Higher-Order Processes

doi:10.1007/s12204-014-1554-y

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

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

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

中图分类号:

TP 301.2

XU Xian1*(徐贤), LONG Huan2 (龙环). A Logical Characterization for Linear Higher-Order Processes[J]. 上海交通大学学报（英文版）, 2015, 20(2): 185-194.

XU Xian1*(徐贤), LONG Huan2 (龙环). A Logical Characterization for Linear Higher-Order Processes[J]. Journal of shanghai Jiaotong University (Science), 2015, 20(2): 185-194.

参考文献 40

[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.