A characterization of regular expressions under bisimulation

ABSTRACT

We solve an open question of Milner [1984]. We define a set of so-called well-behaved finite automata that, modulo bisimulation equivalence, corresponds exactly to the set of regular expressions, and we show how to determine whether a given finite automaton is in this set. As an application, we consider the star height problem.

REFERENCES

• 1: Aceto, L., Fokkink, W., and Verhoef, C. 2001. Structural operational semantics. In Handbook of Process Algebra, J. Bergstra, A. Ponse, and S. Smolka, Eds. Elsevier Science, Amsterdam, The Netherlands, 197--292.
• 2: J. C. M. Baeten , J. A. Bergstra, Global renaming operators in concrete process algebra, Information and Computation, v.78 n.3, p.205-245, Sept. 1988 [doi>10.1016/0890-5401(88)90027-2]
• 3: J. C. M. Baeten , J. A. Bergstra, Process algebra with a zero object, Proceedings on Theories of concurrency : unification and extension: unification and extension, p.83-98, September 1990, Amsterdam, The Netherlands
• 4: J. C. M. Baeten , J. A. Bergstra , J. W. Klop, On the consistency of Koomen's fair abstraction rule, Theoretical Computer Science, v.51 n.1-2, p.129-176, March 31, 1987 [doi>10.1016/0304-3975(87)90052-1 ]
• 5: J. C. M. Baeten , J. A. Bergstra , J. W. Klop, Decidability of bisimulation equivalence for process generating context-free languages, Journal of the ACM (JACM), v.40 n.3, p.653-682, July 1993 [doi>10.1145/174130.174141]
• 6: J. C. M. Baeten , F. Corradini, Regular Expressions in Process Algebra, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), p.12-19, June 26-29, 2005 [doi>10.1109/LICS.2005.43]
• 7: J. C. M. Baeten , C. Verhoef, Concrete process algebra, Handbook of logic in computer science (vol. 4): semantic modelling, Oxford University Press, Oxford, 1995
• 8: J. C. M. Baeten , W. P. Weijland, Process algebra, Cambridge University Press, New York, NY, 1991
• 9: Bergstra, J., Bethke, I., and Ponse, A. 1994. Process algebra with iteration and nesting. Comput. J. 37, 4, 243--258.
• 10: Bergstra, J., Fokkink, W., and Ponse, A. 2001. Process algebra with recursive operations. In Handbook of Process Algebra, J. Bergstra, A. Ponse, and S. Smolka, Eds. Elsevier Science, Amsterdam, The Netherlands, 333--390.
• 11: Jan A. Bergstra , Jan Willem Klop, The Algebra of Recursively Defined Processes and the Algebra of Regular Processes, Proceedings of the 11th Colloquium on Automata, Languages and Programming, p.82-94, July 16-20, 1984
• 12: Bosscher, D. 1997. Grammars modulo bisimulation. Ph.D. University of Amsterdam, Amsterdam, The Netherlands.
• 13: Corradini, F. 2000. A step forward towards equational axiomatizations of Milner bisimulation in Kleene star. In Proceedings FICS 2000.
• 14: Corradini, F., De Nicola, R., and Labella, A. 2002. An equational axiomatization of bisimulation over regular expressions. J. Logic Comput. 12, 301--320.
• 15: Rocco De Nicola , Anna Labella, Nondeterministic regular expressions as solutions of equational systems, Theoretical Computer Science, v.302 n.1-3, p.179-189, 13 June 2003 [doi>10.1016/S0304-3975(02)00774-0]
• 16: Eggan, L. 1963. Transition graphs and the star-height of regular events. Mich. Math. J. 10, 385--397.
• 17: Hashiguchi, K. 1983. Representation theorems on regular languages. J. Comput. Syst. Sci. 27, 101--105.
• 18: Yoram Hirshfeld , Faron Moller, Decidability results in automata and process theory, Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata, p.102-148, April 1996, Banff, Canada
• 19: Yoram Hirshfeld , Faron Moller, On the star height of unary regular behaviours, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 20: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 21: McNaughton, R. 1966. The loop complexity of regular events. Tech. Rep., Machine Structures Group Memo 18, MIT, Cambridge, MA.
• 22: Milner, R. 1984. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci. 28, 3, 439--466.
• 23: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 24: J. E. Pin , H. Straubing , D. Thérien, Some results on the generalized star-height problem, Information and Computation, v.101 n.2, p.219-250, Dec. 1992 [doi>10.1016/0890-5401(92)90063-L]
• 25: Plotkin, G. 2004. A structural approach to operational semantics. J. Logic Algeb. Prog. 60, 17--139. (Reprint from 1981 in Special Issue on Structural Operational Semantics.)
• 26: Géraud Sénizergues, L(A) = L(B)? decidability results from complete formal systems, Theoretical Computer Science, v.251 n.1-2, p.1-166, Jan. 28, 2001 [doi>10.1016/S0304-3975(00)00285-1 ]
• 27: Sewell, P. 1997. Nonaxiomatisability of equivalences over finite state processes. Ann. Pure Appl. Logic 90, 163--191.
• 28: Decidability of DPDA equivalence, Theoretical Computer Science, v.255 n.1-2, p.1-31, March 28, 2001 [doi>10.1016/S0304-3975(00)00389-3 ]
• 29: TeReSe. 2003. Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
• 30: Troeger, D. 1993. Step bisimulation is pomset equivalence on a parallel language without explicit internal choice. Math. Struct. Comput. Sci. 3, 1, 25--62.
• 31: van Beek, D., Man, K., Reniers, M., Rooda, J., and Schiffelers, R. 2006. Syntax and consistent equation semantics of hybrid chi. J. Logic Algeb. Prog. 68, 1/2, 129--210.
• 32: van Glabbeek, R. 2001. The linear time---Branching time spectrum I. The semantics of concrete, sequential processes. In Handbook of Process Algebra, J. Bergstra, A. Ponse, and S. Smolka, Eds. Elsevier Science, Amsterdam, The Netherlands, 3--100.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Relations between models
      F.1.2 Modes of Computation
          Subjects: Interactive and reactive computation

General Terms:
Theory

Keywords:
Bisimulation equivalence, regular expressions