A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra

doi:10.1007/s12204-014-1555-x

上海交通大学学报（英文版） ›› 2015, Vol. 20 ›› Issue (3): 273-280.doi: 10.1007/s12204-014-1555-x

A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra

YANG Fei*(杨非), HUANG Hao (黄浩)

(Laboratory of Basic Studies in Computing Science, Department of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200240, China)

出版日期:2015-06-27 发布日期:2015-06-11
通讯作者: YANG Fei(杨非) E-mail: iamyf@sjtu.edu.cn

A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra

YANG Fei*(杨非), HUANG Hao (黄浩)

(Laboratory of Basic Studies in Computing Science, Department of Computer Science and Engineering, Shanghai Jiaotong University, Shanghai 200240, China)

Online:2015-06-27 Published:2015-06-11
Contact: YANG Fei(杨非) E-mail: iamyf@sjtu.edu.cn

摘要/Abstract

摘要： A polynomial algorithm for the regularity problem of weak and branching bisimilarity on totally normed process algebra (PA) processes is given. Its time complexity is O(n3 + mn), where n is the number of transition rules and m is the maximal length of the rules. The algorithm works for totally normed basic process algebra (BPA) as well as basic parallel process (BPP).

关键词: regularity checking, totally normed process algebra (PA), weak bisimulation

Abstract: A polynomial algorithm for the regularity problem of weak and branching bisimilarity on totally normed process algebra (PA) processes is given. Its time complexity is O(n3 + mn), where n is the number of transition rules and m is the maximal length of the rules. The algorithm works for totally normed basic process algebra (BPA) as well as basic parallel process (BPP).

Key words: regularity checking, totally normed process algebra (PA), weak bisimulation

中图分类号:

TP 301.2

YANG Fei*(杨非), HUANG Hao (黄浩). A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra[J]. 上海交通大学学报（英文版）, 2015, 20(3): 273-280.

YANG Fei*(杨非), HUANG Hao (黄浩). A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra[J]. Journal of shanghai Jiaotong University (Science), 2015, 20(3): 273-280.

参考文献 26

[1]	Hopcroft J, Motwani R, Ullman J. Introduction to automata theory, languages and computation [M].Boston: Addison-Wesley Publishing Company, 1979.
[2]	Park D. Concurrency and automata on infinite sequences[J]. Theoretical Computer Science, 1981, 104:167-183.
[3]	Milner R. Comunication and concurrency [M]. Upper Saddle River, NJ, USA: Prentice Hall, 1989.
[4]	Baeten J C M, Bergstra J A, Klop J W. Decidability of bisimulation equivalence for process generating context-free languages [J]. Journal of the Association for Computing Machinery, 1993, 40(3): 653-682.
[5]	Christensen S, H¨uttel H, Stirling C. Bisimulation equivalence is decidable for all context-free processes[J]. Lecture Notes in Computer Science, 1992,630: 138-147.
[6]	Burkart O, Caucal D, Moller F, et al. Verifcation on infinite structures: Handbook of process algebra[M]. Cambridge: Cambridge University Press, 2001:545-623.
[7]	Moller F, Smolka S, Srba J. On the computational complexity of bisimulation, redux [J]. Information and Computation, 2004, 194(2): 129-143.
[8]	Kuˇcera A, Janˇcar P. Equivalence-checking on infinite-state systems: Techniques and results [J]. Theory and Practice of Logic Programming, 2006, 6(3):227-264.
[9]	Srba J. Roadmap of infinite results [J]. Bullitin in EATCS, 2002 (78): 163-175.
[10]	Mayr R. Process rewrite systems [J]. Information and Computation, 2000, 156(1): 264-286.
[11]	Burkart O, Caucal D, Steffen B. An elementary bisimulation decision procedure for arbitrary contextfree processes [J]. Mathematical Foundations of Computer Science, 1995, 969: 423-433.
[12]	Hirshfeld Y, Jerrum M, Moller F. A polynomial algorithm for deciding bisimilarity of normed contextfree processes [J]. Journal of Theoretical Computer Science,1996, 158(1): 143-159.
[13]	Kuˇcera A. Regularity is decidable for normed PA processes in polynomial time [C]//Foundations of Software Technology and Theoretical Computer Science.Geneva: Springer-Verlag, 1996: 111-122.
[14]	Janˇcar P. Strong bisimilarity on basic parallel processes in PSPACE-complete [C]//Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science.Edinburgh: IEEE, 2003: 218-227.
[15]	Kot M. Regularity of BPP is PSPACE-complete [C]//Proceedings of the 3rd Ph. D. Workshop of Faculty of Electrical Engineering and Computer Science(WOFEX’05). Ostrava: VSB-Technical University of Ostravay, 2005: 393-398.
[16]	Hirshfeld Y, Jerrum M, Moller F. A polynomialtime algorithm for deciding bisimulation equivalence of normed basic parallel processes [J]. Mathematical Structures in Computer Science, 1996, 6(3): 251-259.
[17]	Hirshfeld Y, Jerrum M. Bisimulation equivalence is decidable for normed process algebra [J]. Automata,Languages and Programming, 1999, 1644: 412-421.
[18]	Czerwi′nski W, Hofman P, Lasota S. Decidability of branching bisimulation on normed commutative context-free processes [J]. Lecture Notes in Computer Science, 2011, 6901: 528-542.
[19]	Fu Y. Checking equality and regularity for normed BPA with silent moves [J]. Automata, Languages, and Programming, 2013, 7966: 238-249.
[20]	H¨uttel H. Silence is golden: Branching bisimilarity is decidable for context-free processes [J]. Lecture Notes in Computer Science, 1992, 575: 2-12.
[21]	Chen H. Decidability of weak bisimilarity for a subset of BPA [J]. Electronic Notes in Theoretical Computer Science, 2008, 212: 241-255.
[22]	Chen H. More on weak bisimilarity of normed basic parallel processes [J]. Theory and Applications of Models of Computation, 2008, 4978: 192-203.
[23]	van Glabbeek R, Weijland W. Branching time and abstraction in bisimulation semantics [J]. Journal of the Association for Computing Machinery, 1996,43(3): 555-600.
[24]	Srba J. Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard [J]. Lecture Notes in Computer Science, 2002, 2285: 535-546.
[25]	Mayr R. Weak bisimilarity and regularity of BPA is EXPTIME-hard [C]//Proccedings of the 10th International Workshop on Expressiveness in Concurrency(EXPRESS’03). Marseilles, France: Elsevier Science Publishers, 2003: 160-143.
[26]	Srba J. Complexity of weak bisimilarity and regularity for BPA and BPP [J]. Electronic Notes in Theoretical Computer Science, 2003, 39(1): 79-93.

A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra

A Polynomial Time Algorithm for Checking Regularity of Totally Normed Process Algebra

可视化

摘要/Abstract

引用本文

使用本文

参考文献 26

相关文章 5

编辑推荐

Metrics

本文评价

[1]	WU Xing* (武星), Lü Hai-tao (吕海涛), ZHUO Shao-jian (卓少剑). Sentiment Analysis for Chinese Text Based on Emotion Degree Lexicon and Cognitive Theories[J]. 上海交通大学学报（英文版）, 2015, 20(1): 1-6.
[2]	CHEN Jun-qing* (陈俊清), HUANG Lin-peng (黄林鹏), YU Cheng-yuan (于程远). Behavior-Consistent Service Substitutions in Dynamic Environments[J]. 上海交通大学学报（英文版）, 2014, 19(1): 17-27.
[3]	YIN Qiang* (尹强), LONG Huan (龙环). Process Passing Calculus, Revisited[J]. 上海交通大学学报（英文版）, 2013, 18(1): 29-36.
[4]	JIN Yun (金云). External Equality and Absolute Equality Coincide in Finite CCS and π Calculus Without Summation[J]. 上海交通大学学报（英文版）, 2011, 16(5): 533-537.
[5]	XU Xian1*(徐贤), LONG Huan2 (龙环). A Logical Characterization for Linear Higher-Order Processes[J]. 上海交通大学学报（英文版）, 2015, 20(2): 185-194.