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

doi:10.1007/s12204-014-1555-x

Abstract

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

摘要： 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

CLC Number:

TP 301.2

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.

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