Skip to main content
SpringerLink
Log in

Dihomotopy as a Tool in State Space Analysis Tutorial

  • Conference paper
  • First Online:
LATIN 2002: Theoretical Informatics (LATIN 2002)

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

Included in the following conference series:

Abstract

Recent geometric methods have been used in concurrency theory for quickly finding deadlocks and unreachable states, see [14 ] for instance. The reason why these methods are fast is that they contain in germ ingredients for tackling the state-space explosion problem. In this paper we show how this can be made formal. We also give some hints about the underlying algorithmics. Finally, we compare with other well-known methods for coping with the state-space explosion problem.

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. M.A. Armstrong, Basic Topology, Springer-Verlag, 1990.

    Google Scholar 

  2. M.A. Bednarczyk. Categories of asynchronous systems. PhD thesis, University of Sussex, 1988.

    Google Scholar 

  3. Bernard Boigelot and Patrice Godefroid. Symbolic verification of communication protocols with in finite state spaces using QDDs.Formal Methods in System Design: An International Journal, 14(3):237–255, May 1999.

    Article  Google Scholar 

  4. T. Borceux, Handbookof Categorial Algebra I:Basic category theory, Encyclopedia of Mathematics and its Applications, Cambridge University Press, 1994.

    Google Scholar 

  5. Glen E. Bredon, Topology and Geomery, GTM, vol. 139, Springer-Verlag, 1993.

    Google Scholar 

  6. R. Brown and P.J. Higgins, Colimi heorems for relative homotopy groups, J. Pure Appl. Algebra 22 (1981), 11–41.

    Article  MathSciNet  Google Scholar 

  7. -,On the algebra of cubes, J. Pure Appl. Algebra 21 (1981), 233–260.

    Article  MathSciNet  Google Scholar 

  8. S.D. Carson and P.F. Reynolds, The geometry of semaphore programs, ACM TOPLAS 9 (1987), no.1, 25–53.

    Article  Google Scholar 

  9. E.M. Clarke, E.A. Emerson, S. Jha, and A.P. Sistla. Symmetry reductions in model checking. In Proc.10th International Computer Aided Verification Conference, pages 145–458, 1998.

    Google Scholar 

  10. E.G. Coffman, M.J. Elphick, and A. Shoshani. System deadlocks.Computing Surveys, 3(2):67–78, June 1971.

    Article  Google Scholar 

  11. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. Principles of Programming Languages 4, pages 238–252, 1977.

    Google Scholar 

  12. E.W. Dijkstra, Co-operating sequential processes, Programming Languages (F. Genuys,ed.), Academic Press, New York, 1968, pp.43–110.

    Google Scholar 

  13. L. Fajstrup, Dicovering spaces, Tech. Report R-01-2023, Department of Mathematical Sciences, Aalborg University, DK-9220 AalborgØst, November 2001.

    Google Scholar 

  14. L. Fajstrup, É. Goubault, and M. Raussen, Detecting Deadlocks in Concurrent Systems, CONCUR’ 98; Concurrency Theory (Nice, France)(D. Sangiorgi and R. de Simone,eds.), Lect.Notes Comp.Science,vol.1466, Springer-Verlag, September 1998, 9th Int.Conf., Proceedings, pp.332–347.

    Google Scholar 

  15. L. Fajstrup, E. Goubault, and M. Raussen.Detecting deadlocks in concurrent systems.Technical report, CEA, 1998.

    Google Scholar 

  16. -, Algebraic opology and concurrency, Tech.Report R-99-2008, Department of Mathematical Sciences, Aalborg University, DK-9220 AalborgØst, June 1999, conditionally accepted for publication in Theoret.Comput. Sci.

    Google Scholar 

  17. L. Fajstrup and S. Sokolowski, Infinitely running concurrents processes with loops from a geometric viewpoin, Electronic Notes Theor. Comput. Sci. 39 (2000), no.2, 19 pp.,URL:http://www.elsevier.nl/locate/entcs/volume39.html.

    Article  Google Scholar 

  18. P. Gabriel and M. Zisman, Calculus of fractions and homotopy theory, Springer-Verlag New York, Inc., New York, 1967, Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 35.

    Google Scholar 

  19. P. Gaucher, Homotopy invariants of higher dimensional categories and concurrency in computer science, Math. Structures Comput. Sci.10 (2000), no.4, 481–524.

    Article  MathSciNet  Google Scholar 

  20. P. Godefroid, G.J. Holzmann, and D. Pirottin. State space caching revisited. In Proc.4th International Computer Aided Verification Conference, pages 178–191, 1992.

    Google Scholar 

  21. P. Godefroid and P. Wolper, Using partial orders for the efficient verification of deadlockfreedom and safety properties, Proc.of the Third Workshop on Computer Aided Verification, vol.575, Springer-Verlag, Lecture Notes in Computer Science, 1991, pp.417–428.

    Google Scholar 

  22. P. Godefroid and P. Wolper. Partial-order methods for temporal verification. In Proc.of CONCUR’ 93. Springer-Verlag, LNCS, 1993.

    MATH  Google Scholar 

  23. É. Goubault, The Geometry of Concurrency, Ph.D.thesis, Ecole Normale Superieure, Paris, 1995.

    Google Scholar 

  24. -, Geometry and Concurrency: A User’s Guide, Electronic Notes Theor. Comput.Sci. 39 (2000), no.2, 16 pp.,URL: http://www.elsevier.nl/locate/entcs/volume39.html.

  25. -, Cubical sets are generalized transition systems, avail. at http://www.di.ens.fr/~goubault 2001.

  26. J. Gunawardena, Homotopy and concurrency, Bulletin of the EATCS 54 (1994), 184–193.

    MATH  Google Scholar 

  27. A. Hatcher, Algebraic Topology, electronically avialable at http://www.math.cornell.edu/~hatcher/# ATI

  28. T.A. Henzinger, O. Kupferman, and S. Qadeer. From pre-historic to post-modern symbolic model checking. In Proc.10th International Computer Aided Verification Conference, pages 195–206.,1998.

    Google Scholar 

  29. M. Herlihy, S. Rajsbaum, and M. Tuttle, An Overview of synchronous Message-Passing and Topology, Electronic Notes Theor.Comput.Sci.39 (2000), no.2.

    Article  Google Scholar 

  30. P.J. Higgins, Categories and Groupoids, Mathematical Studies,vol.32,van Nortrand Reinhold, London,1971.

    Google Scholar 

  31. G. Holzmann.On-the-fly model checking.ACM Computing Surveys, 28(4es):120–120, December 1996.

    Google Scholar 

  32. W. Lipski and C.H. Papadimitriou, A fast algori hm for esting for safety and detecting deadlocks in locked transaction systems, Journal of Algorithms 2 (1981), 211–226.

    Article  MathSciNet  Google Scholar 

  33. S. Mac Lane, Categories for he working mathematician, Graduate Texts in Mathematics, vol.5, Springer-Verlag, New York, Heidelberg, Berlin, 1971.

    Book  Google Scholar 

  34. A. Mazurkiewicz. Trace theory.In G. Rozenberg, editor, Petri Nets: Applications and Relationship to Other Models of Concurrency, Advances in Petri Nets 1986, PART II, PO of an Advanced Course, volume 255 of LNCS, pages 279–324, Bad Honnefs, September 1986. Springer-Verlag.

    Google Scholar 

  35. J.R. Munkres, Elements of Algebraic Topology, Addison-Wesley,1984.

    Google Scholar 

  36. V. Pratt, Modelling concurrency with geometry, Proc.of the 18th ACM Symposium on Principles of Programming Languages.(1991).

    Google Scholar 

  37. M. Raussen, On the classification of dipaths in geometric models for concurrency, Math.Structures Comput.Sci.10 (2000), no.4, 427–457.

    Article  MathSciNet  Google Scholar 

  38. -, State spaces and dipaths up to dihomotopy, Tech.Report R-01-2025, Department of Mathematical Sciences, Aalborg University, DK-9220 Aalborg Øst, November 2001.

    Google Scholar 

  39. V. Sassone and G.L. Cattani. Higher-dimensional transition systems. In Proceedings of LICS’ 96, 1996.

    Google Scholar 

  40. V. Sassone, M. Nielsen, and G. Winskel. Relationships between models of concurrency. In Proceedings of he Rex’ 93 school and symposium, 1994.

    Google Scholar 

  41. J.P. Serre, Homologie singulière des espaces fibrés., Ann.of Math.(2) 54 (1951), 425–505.

    Article  MathSciNet  Google Scholar 

  42. A. Shoshani and E.G. Coffman. Sequencing tasks in multiprocess systems to avoid deadlocks. In Conference Record of 1970 Eleventh Annual Symposium on Switching and Automata Theory, pages 225–235, Santa Monica,California,Oct 1970.IEEE.

    Google Scholar 

  43. S. Sokołowski, Categories of dimaps and heir dihomotopies in po-spaces and local po-spaces, Preliminary Proceedings of the Workshop on Geometry and Topology in Concurrency Theory GETCO’ 01 (Aalborg,Denmark) (P. Cousot et al.,ed.), vol. NS-01, BRICS Notes Series, no.7, BRICS, 2001, pp.77–97.

    Google Scholar 

  44. J. Srba, On the Power of Labels in Transition Systems, CONCUR 2001 (Aalborg, Denmark)(K.G. Larsen and M. Nielsen, eds., Lect.Notes Comp.Science, vol. 2154, Springer-Verlag, 2001, pp.277–291.

    Google Scholar 

  45. A. Stark.Concurrent transition systems.Theoretical Computer Science, 64:221–269, 1989.

    Article  MathSciNet  Google Scholar 

  46. A. Valmari, A stubborn attackon state explosion, Proc.of Computer Aided Verification, no.3, AMS DIMACS series in Discrete Mathematics and Theoretical Computer Science, 1991, pp.25–41.

    Google Scholar 

  47. R. van Glabbeek, Bisimulation semantics for higher dimensional automata, Tech. report, Stanford University,1991.

    Google Scholar 

  48. R. van Glabbeek and U Goltz. Partial order semantics for refinement of actions. Bulle in of he EATCS, (34), 1989.

    Google Scholar 

  49. F. Vernadat, P. Azema, and F. Michel. Covering step graph.Lecture Notes in Computer Science, 1091, 1996.

    Google Scholar 

  50. G. Winskel and M. Nielsen. Models for concurrency, volume 3 of Handbook of Logic in Computer Science.Oxford University Press, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIST (CEA Saclay), DTSI-SLA-LSL, 91191, Gif-sur-Yvette, France

    Éric Goubault

  2. Institute of Mathematical Sciences, Aalborg University, 9220, Aalborg Øst, Denmark

    Marti Raussen

Authors
  1. Éric Goubault
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marti Raussen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Compaq Cambridge Research Laboratory, One Cambridge Center, 02142-1612, Cambridge, MA, USA

    Sergio Rajsbaum

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goubault, É., Raussen, M. (2002). Dihomotopy as a Tool in State Space Analysis Tutorial. In: Rajsbaum, S. (eds) LATIN 2002: Theoretical Informatics. LATIN 2002. Lecture Notes in Computer Science, vol 2286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45995-2_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-45995-2_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45995-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation