J Shanghai Jiaotong Univ Sci

Journal of Shanghai Jiaotong University(Science) >

2015 , Vol. 20 >Issue 3: 273 - 280

DOI: https://doi.org/10.1007/s12204-014-1555-x

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

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

Online published: 2015-06-11

Fold

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

Cite this article

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 . DOI: 10.1007/s12204-014-1555-x

References

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

/

〈 〉