Skip to main content
SpringerLink
Log in

Deciding Bisimilarity between BPA and BPP Processes

  • Conference paper
Book cover CONCUR 2003 - Concurrency Theory (CONCUR 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2761))

Included in the following conference series:

Abstract

We identify a necessary condition for when a given BPP process can be expressed as a BPA process. We provide an effective procedure for testing if this condition holds of a given BPP, and in the positive case we provide an effective construction for a particular form of one-counter automaton which is bisimilar to the given BPP. This in turn provides the mechanism to decide bisimilarity between a given BPP process and a given BPA process.

The first two authors are supported by the Grant Agency of the Czech Republic, grant No. 201/03/1161.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Decidability of bisimulation equivalence for processes generating context-free languages. Journal of the ACM 40(3), 653–682 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  2. Blanco, J.: Normed BPP and BPA. In: Proceedings of ACP 1994, pp. 242–251. Springer, Heidelberg (1995)

    Google Scholar 

  3. Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra. ch. 9, pp. 545–623. Elsevier Science, Amsterdam (2001)

    Chapter  Google Scholar 

  4. Burkart, O., Caucal, D., Steffen, B.: An elementary decision procedure for arbitrary contextfree processes. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 423–433. Springer, Heidelberg (1995)

    Google Scholar 

  5. Černá, I., Křetínský, M., Kučera, A.: Comparing expressibility of normed BPA and normed BPP processes. Acta Informatica 36, 233–256 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  6. Glabbeek, R.: The linear time – branching time spectrum I: The semantics of concrete sequential processes. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra. ch. 1, pp. 3–99. Elsevier Science, Amsterdam (2001)

    Chapter  Google Scholar 

  7. Hirshfeld, Y., Jerrum, M.: Bisimulation equivalence is decidable for normed process algebra. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 412–421. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science 158, 143–159 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  9. Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial-time algorithm for deciding bisimulation equivalence of normed basic parallel processes. Journal of Mathematical Structures in Computer Science 6, 251–259 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  10. Jančar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science 148(2), 281–301 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  11. Jančar, P.: Strong bisimilarity on basic parallel processes is PSPACE-complete. In: Proceedings of LICS 2003 (2002) (to appear)

    Google Scholar 

  12. Jančar, P., Kučera, A.: Equivalence-checking with infinite-state systems: Techniques and results. In: Grosky, W.I., Plášil, F. (eds.) SOFSEM 2002. LNCS, vol. 2540, pp. 41–73. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Jančar, P., Moller, F.: Techniques for decidability and undecidability of bisimilarity. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 30–45. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Karp, R.M., Miller, R.E.: Parallel Program Schemata. Journal of Computer and Systems Sciences 3, 147–195 (1969)

    Article  MATH  MathSciNet  Google Scholar 

  15. Milner, R., Moller, F.: Unique decomposition of processes. Theoretical Computer Science 107, 357–363 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  16. Moller, F.: Infinite results. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 195–216. Springer, Heidelberg (1996)

    Google Scholar 

  17. Sénizergues, G.: Decidability of bisimulation equivalence for equational graphs of finite outdegree. In: Proceedings of FOCS 1998, pp. 120–129. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  18. Sénizergues, G.: L(A)=L(B)? decidability results from complete formal systems. Theoretical Computer Science 251(1-2), 1–166 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  19. Srba, J.: Roadmap of Infinite Results, http://www.brics.dk/~srba/roadmap

  20. Srba, J.: Strong bisimilarity and regularity of basic process algebra is PSPACE-hard. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 716–727. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Srba, J.: Strong bisimilarity and regularity of basic parallel processes is PSPACE-hard. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 535–546. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  22. Stirling, C.: Decidability of bisimulation equivalence for pushdown processes. Research Report No. EDI-INF-RR-0005, School of Informatics, Edinburgh University (January 2000)

    Google Scholar 

  23. Stirling, C.: Decidability of DPDA equivelance. Theoretical Computer Science 255(1-2), 1–31 (2001)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, FEI, Technical University of Ostrava, 17. listopadu 15, 70833, Ostrava, Czech Republic

    Petr Jančar

  2. Faculty of Informatics, Masaryk University, Botanická 68a, 60200, Brno, Czech Republic

    Antonín Kučera

  3. Dept. of Computer Science, University of Wales Swansea, Singleton Park, Swansea, Wales, SA2 8PP

    Faron Moller

Authors
  1. Petr Jančar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antonín Kučera
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Faron Moller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Université Paris 7, PPS, Case 7014, 75205, Paris Cedex 13, France

    Roberto Amadio

  2. LIF, CNRS, Aix-Marseille Université, France

    Denis Lugiez

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jančar, P., Kučera, A., Moller, F. (2003). Deciding Bisimilarity between BPA and BPP Processes. In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45187-7_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40753-9

  • Online ISBN: 978-3-540-45187-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation