Skip to main content
SpringerLink
Log in

Decidability of Strong Bisimilarity for Timed BPP

  • Conference paper
  • First Online:
CONCUR 2002 — Concurrency Theory (CONCUR 2002)

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

Included in the following conference series:

Abstract

We investigate a timed extension of the class of Basic Parallel Processes (BPP), in which actions are durational and urgent and parallel components have independent local clocks. The main result is decidability of strong bisimilarity, known also as performance equivalence, in this class. This extends the earlier decidability result for plain BPP [8] as well as decidability for timed BPP with strictly positive durations of actions [3]. Both ill-timed and well-timed semantics are treated. Our decision procedure is based on decidability of the validity problem for Presburger arithmetic.

This work has been supported by the fellowship of the Foundation for Polish Science, during the author’s post-doc stay at Laboratoire Specification et Verification, ENS Cachan. Partially supported by the KBN grant 7 T11C 002 21 and by the Research Training Network Games.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. L. Aceto and D. Murphy. Timing and causality in process algebra. Acta Informatica, 33(4):317–350, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  2. J. C. M. Baeten and C. A. Middelburg. Process algebra with timing: real time and discrete time. In J. Bergstra, A. Ponse, S. Smolka, eds., Handbook of Process Algebra, chapter 10, pages 627–684, 2001.

    Google Scholar 

  3. B. Bérard, A. Labroue, and P. Schnoebelen. Verifying performance equivalence for timed Basic Parallel Processes. In Proc. 3rd Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS’2000), LNCS 1784, pages 35–47, 2000.

    Google Scholar 

  4. O. Burkart, D. Caucal, F Moller, and B. Steffen. Verification of infinite structures. In J. Bergstra, A. Ponse, S. Smolka, eds., Handbook of Process Algebra, chapter 9, pages 545–623, 2001.

    Google Scholar 

  5. D. Caucal. Graphes canoniques des graphes algebraiques. Informatique Theoretique et Applications (RAIRO), 24(4):339–352, 1990.

    MATH  MathSciNet  Google Scholar 

  6. K. Čerāns. Decidability of bisimulation equivalence for parallel timer processes. In Proc. CAV’92, LNCS 663, 1992.

    Google Scholar 

  7. S. Christensen. Decidability and Decomposition in process algebras. PhD thesis, Dept. of Computer Science, University of Edinbourg, UK, 1993. PhD Thesis CST-105-93.

    Google Scholar 

  8. S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation equivalence is decidable for Basic Parallel Processes. In Proc. 4th Int. Conf. Concurrency Theory (CONCUR’ 93), LNCS 713, pages 143–157, 1993.

    Google Scholar 

  9. F. Corradini. On performance congruences for process algebras. Information and Computation, 145(2):191–230, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  10. F. Corradini, R. Gorrieri, and M. Roccetti. Performance preorder and competitive equivalence. Acta Informatica, 34(11):805–835, 1997.

    Article  MathSciNet  Google Scholar 

  11. F. Corradini and M. Pistore. Specification and verification of lazy timed systems. In Proc. 21th Int. Symp. math. Found. Comp. Sci. (MFCS’96), LNCS 1113, pages 279–290, 1996.

    Google Scholar 

  12. S. Eilenberg and M. P. Schuetzenberger. Rational sets in commutative monoids. J. of Algebra, 13:173–191, 1969.

    Article  MATH  Google Scholar 

  13. S. Ginsburg and E. Spanier. Semigroups, Presburger formulas, and languages. Pacific J. of Mathematics, 16(2):285–296, 1966.

    MATH  MathSciNet  Google Scholar 

  14. R. Gorrieri, M. Roccetti, and E. Stancampiano. A theory of processes with durational actions. Theoretical Computer Science, 140(1):73–94, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  15. Y. Hirshfeld. Petri nets and the equivalence problem. In Proc. Computer Science Logic (CSL’93), LNCS 832, pages 165–174, 1993.

    Google Scholar 

  16. Y. Hirshfeld. Congruences in commutative semigroups. LFCS report ECS-LFCS-94-291, Laboratory for Foundations of Computer Science, University of Edinbourg, 1994.

    Google Scholar 

  17. H. Hüttel. Undecidable equivalences for basic parallel processes. In Proc. TACS’94, LNCS 789, pages 454–464, 1994.

    Google Scholar 

  18. P. Jančar. Decidability questions for bisimilarity of Petri nets and some related problems. In Proc. 11th International Symposium on Theoretical Aspects of Computer Science (STACS’94), Caen, France, LNCS 775, pages 581–592, 1994.

    Google Scholar 

  19. R. Milner. Communication and Concurrency. Prentice Hall, 1989.

    Google Scholar 

  20. F. Moller and C. Tofts. Relating processes with respect to speed. In Proc. 2nd Int Conf. Concurrency Theory (CONCUR’91), LNCS 527, pages 424–438, 1991.

    Google Scholar 

  21. D. C. Oppen. A 22 2 pn upper bound on the complexity of Presburger arithmetic. J. of Comp. and System Sciences, 16:323–332, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  22. J. Srba. Note on the tableau technique for commutative transition systems. In Proc. 5th Foundations of Software Science and Computation Structures (FOSSACS’02), LNCS 2303, pages 387–401, 2002.

    Google Scholar 

  23. J. Srba. Strong bisimilarity and regularity of Basic Parallel Processes is PSPACEhard. In Proc. 19th International Symposium on Theoretical Aspects of Computer Science (STACS’02), LNCS 2285, 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, CNRS UMR 8643 & ENS Cachan, France

    Sławomir Lasota

  2. Institute of Informatics, Warsaw University, Poland

    Sławomir Lasota

Authors
  1. Sławomir Lasota
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Masaryk University Brno, Botanicka 68a, 60200, Brno, Czech Republic

    Luboš Brim , Mojmír Křetínský  & Antonín Kučera ,  & 

  2. Faculty of Electrical Engineering and Informatics, Department of Computer Science, Technical University of Ostrava (VSB), 17. listopadu 15, 70833, Ostrava-Poruba, Czech Republic

    Petr Jančar

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lasota, S. (2002). Decidability of Strong Bisimilarity for Timed BPP. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds) CONCUR 2002 — Concurrency Theory. CONCUR 2002. Lecture Notes in Computer Science, vol 2421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45694-5_37

Download citation

  • DOI: https://doi.org/10.1007/3-540-45694-5_37

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44043-7

  • Online ISBN: 978-3-540-45694-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation