Journal of shanghai Jiaotong University (Science) ›› 2015, Vol. 20 ›› Issue (2): 185-194.doi: 10.1007/s12204-014-1554-y
Previous Articles Next Articles
XU Xian1*(徐贤), LONG Huan2 (龙环)
Published:
2015-04-02
Contact:
XU Xian(徐贤)
E-mail:xuxian@ecust.edu.cn
CLC Number:
XU Xian1*(徐贤), LONG Huan2 (龙环). A Logical Characterization for Linear Higher-Order Processes[J]. Journal of shanghai Jiaotong University (Science), 2015, 20(2): 185-194.
[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. |
[1] | SHI Huirong, WANG Haixing, LI Zonggang. Stability of Orthogonal Cutting System Considering Nonlinear Stiffness [J]. Journal of Shanghai Jiao Tong University, 2022, 56(2): 191-200. |
[2] | WANG Lipo. Quantification of Spatial Structures of Complex Systems [J]. Journal of Shanghai Jiao Tong University, 2021, 55(Sup.1): 104-105. |
[3] | LIU Xin ∗ (刘鑫), WANG Lixiao (王力晓), CHEN Qidong (陈启东), SUN Beibei (孙蓓蓓). Parameter Identification of Structural Nonlinearity by Using Response Surface Plotting Technique [J]. J Shanghai Jiaotong Univ Sci, 2021, 26(6): 819-827. |
[4] | MA Zhe,ZHOU Ting,SUN Jiawen,FANG Kezhao,ZHAI Gangjun. Numerical Simulation of Nonlinear Wave Based on an Improved Source Wave Method [J]. Journal of Shanghai Jiaotong University, 2020, 54(1): 60-68. |
[5] | ZHANG Shuo,YE Guanlin,ZHEN liang,LI Mingguang,CHEN Chaobin. Constitutive Model of Soft Soil After Considering Small Strain Stiffness Decay Characteristics [J]. Journal of Shanghai Jiaotong University, 2019, 53(5): 535-539. |
[6] | ZHANG Guang,WANG Huixing,OUYANG Qing,WANG Jiong. Thermal and Fluid Coupling Field Analysis of MR Damper for Gun Recoil [J]. Journal of Shanghai Jiaotong University, 2019, 53(4): 504-512. |
[7] | GUO Huiyong,HUANG Qi. Time-Domain Nonlinear Damage Detection Based on GARCH Effect and Improved Penalty Index [J]. Journal of Shanghai Jiaotong University, 2019, 53(11): 1326-1334. |
[8] | WANG Zhenyu (王振瑜), WU Xiaosheng * (吴校生), SHU Shengzhu (叔晟竹) . Resonance Characteristics of Piezoelectric Resonator Based on Digital Driving Circuit of Field-Programmable Gate Array [J]. Journal of Shanghai Jiao Tong University (Science), 2019, 24(1): 1-6. |
[9] | JIN Jing,YANG Zhaolin,LIU Litong,ZHOU Jianjun. Fully-Integrated Reconfigurable CMOS Global Navigation Satellite System Receivers with High-Linearity [J]. Journal of Shanghai Jiaotong University, 2018, 52(10): 1226-1233. |
[10] | CHEN Si,MA Ning,GU Xiechong. Numerical Calculation of Added Resistance of Ships in#br# Waves Based on Weakly Nonlinear Assumption [J]. Journal of Shanghai Jiaotong University, 2017, 51(3): 277-. |
[11] | JIANG Sheng-chao-, ZONG Zhi, ZOU Li. Wave Resonance between Two Ships with Non-Identical Draft [J]. Ocean Engineering Equipment and Technology, 2017, 4(3): 150-156. |
[12] | ZOU Ke, CHEN Jin-long, YUAN Zhen-qin. Effect of Buoyancy Modules’ Bending Stiffness Behavior on Flexible Riser in Shallow Water [J]. Ocean Engineering Equipment and Technology, 2016, 3(5): 287-291. |
[13] | ZHENG Xiaoya1*(郑晓亚), YOU Haibo2 (尤海波). Do China Mainland and SARs Constitute an Optimal Currency Area? Evidence from Nonlinearity and Stationarity Behavior Testing on Real Exchange Rates [J]. Journal of shanghai Jiaotong University (Science), 2016, 21(3): 328-334. |
[14] | REN Shaofei, TANG Wenyong, XUE Hongxiang. Numerical Method to Predict Failure of Carcass Layer of Unbonded Flexible Risers [J]. Journal of Shanghai Jiao Tong University, 2016, 50(03): 465-471. |
[15] | LIU Weiguang,YU Yin,WANG Hai. A Damage Model Considering Shear Nonlinearity for Progressive Failure Analysis of Composite Laminates [J]. Journal of Shanghai Jiaotong University, 2016, 50(02): 194-199. |
Viewed | ||||||
Full text |
|
|||||
Abstract |
|
|||||