{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:44Z","timestamp":1761611204208},"publisher-location":"Berlin, Heidelberg","reference-count":50,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434009"},{"type":"electronic","value":"9783540459958"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45995-2_8","type":"book-chapter","created":{"date-parts":[[2007,5,30]],"date-time":"2007-05-30T02:33:34Z","timestamp":1180492414000},"page":"16-37","source":"Crossref","is-referenced-by-count":15,"title":["Dihomotopy as a Tool in State Space Analysis Tutorial"],"prefix":"10.1007","author":[{"given":"\u00c9ric","family":"Goubault","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marti","family":"Raussen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"8_CR1","unstructured":"M.A. Armstrong, Basic Topology, Springer-Verlag, 1990."},{"key":"8_CR2","unstructured":"M.A. Bednarczyk. Categories of asynchronous systems. PhD thesis, University of Sussex, 1988."},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1008719024240","volume":"14","author":"B. Boigelot","year":"1999","unstructured":"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\u2013255, May 1999.","journal-title":"Formal Methods in System Design: An International Journal"},{"key":"8_CR4","unstructured":"T. Borceux, Handbookof Categorial Algebra I:Basic category theory, Encyclopedia of Mathematics and its Applications, Cambridge University Press, 1994."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Glen E. Bredon, Topology and Geomery, GTM, vol. 139, Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4757-6848-0"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-4049(81)90080-3","volume":"22","author":"R. Brown","year":"1981","unstructured":"R. Brown and P.J. Higgins, Colimi heorems for relative homotopy groups, J. Pure Appl. Algebra 22 (1981), 11\u201341.","journal-title":"J. Pure Appl. Algebra"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0022-4049(81)90018-9","volume":"21","author":"R. Brown","year":"1981","unstructured":"-,On the algebra of cubes, J. Pure Appl. Algebra 21 (1981), 233\u2013260.","journal-title":"J. Pure Appl. Algebra"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/9758.9759","volume":"9","author":"S.D. Carson","year":"1987","unstructured":"S.D. Carson and P.F. Reynolds, The geometry of semaphore programs, ACM TOPLAS 9 (1987), no.1, 25\u201353.","journal-title":"ACM TOPLAS"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013458, 1998.","DOI":"10.1007\/BFb0028741"},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/356586.356588","volume":"3","author":"E.G. Coffman","year":"1971","unstructured":"E.G. Coffman, M.J. Elphick, and A. Shoshani. System deadlocks.Computing Surveys, 3(2):67\u201378, June 1971.","journal-title":"Computing Surveys"},{"key":"8_CR11","first-page":"238","volume":"4","author":"P. Cousot","year":"1977","unstructured":"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\u2013252, 1977.","journal-title":"Principles of Programming Languages"},{"key":"8_CR12","first-page":"43","volume-title":"Co-operating sequential processes, Programming Languages","author":"E.W. Dijkstra","year":"1968","unstructured":"E.W. Dijkstra, Co-operating sequential processes, Programming Languages (F. Genuys,ed.), Academic Press, New York, 1968, pp.43\u2013110."},{"key":"8_CR13","unstructured":"L. Fajstrup, Dicovering spaces, Tech. Report R-01-2023, Department of Mathematical Sciences, Aalborg University, DK-9220 Aalborg\u00d8st, November 2001."},{"key":"8_CR14","unstructured":"L. Fajstrup, \u00c9. Goubault, and M. Raussen, Detecting Deadlocks in Concurrent Systems, CONCUR\u2019 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\u2013347."},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"L. Fajstrup, E. Goubault, and M. Raussen.Detecting deadlocks in concurrent systems.Technical report, CEA, 1998.","DOI":"10.1007\/BFb0055632"},{"key":"8_CR16","unstructured":"-, Algebraic opology and concurrency, Tech.Report R-99-2008, Department of Mathematical Sciences, Aalborg University, DK-9220 Aalborg\u00d8st, June 1999, conditionally accepted for publication in Theoret.Comput. Sci."},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S1571-0661(05)01147-3","volume":"39","author":"L. Fajstrup","year":"2000","unstructured":"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.","journal-title":"Electronic Notes Theor. Comput. Sci"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-3-642-85844-4"},{"issue":"4","key":"8_CR19","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1017\/S0960129500003182","volume":"10","author":"P. Gaucher","year":"2000","unstructured":"P. Gaucher, Homotopy invariants of higher dimensional categories and concurrency in computer science, Math. Structures Comput. Sci.10 (2000), no.4, 481\u2013524.","journal-title":"Math. Structures Comput. Sci"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"P. Godefroid, G.J. Holzmann, and D. Pirottin. State space caching revisited. In Proc.4th International Computer Aided Verification Conference, pages 178\u2013191, 1992.","DOI":"10.1007\/3-540-56496-9_15"},{"key":"8_CR21","series-title":"Lect Notes Comput Sci","first-page":"417","volume-title":"Using partial orders for the efficient verification of deadlockfreedom and safety properties","author":"P. Godefroid","year":"1991","unstructured":"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\u2013428."},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Partial-order methods for temporal verification","author":"P. Godefroid","year":"1993","unstructured":"P. Godefroid and P. Wolper. Partial-order methods for temporal verification. In Proc.of CONCUR\u2019 93. Springer-Verlag, LNCS, 1993."},{"key":"8_CR23","unstructured":"\u00c9. Goubault, The Geometry of Concurrency, Ph.D.thesis, Ecole Normale Superieure, Paris, 1995."},{"key":"8_CR24","unstructured":"-, Geometry and Concurrency: A User\u2019s Guide, Electronic Notes Theor. Comput.Sci. 39 (2000), no.2, 16 pp.,URL: http:\/\/www.elsevier.nl \/locate\/entcs\/volume39.html."},{"key":"8_CR25","unstructured":"-, Cubical sets are generalized transition systems, avail. at http:\/\/www.di.ens.fr \/~goubault 2001."},{"key":"8_CR26","first-page":"184","volume":"54","author":"J. Gunawardena","year":"1994","unstructured":"J. Gunawardena, Homotopy and concurrency, Bulletin of the EATCS 54 (1994), 184\u2013193.","journal-title":"Bulletin of the EATCS"},{"key":"8_CR27","unstructured":"A. Hatcher, Algebraic Topology, electronically avialable at http:\/\/www.math.cornell.edu \/~hatcher\/# ATI"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"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\u2013206.,1998.","DOI":"10.1007\/BFb0028745"},{"issue":"2","key":"8_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S1571-0661(05)01148-5","volume":"39","author":"Maurice Herlihy","year":"2000","unstructured":"M. Herlihy, S. Rajsbaum, and M. Tuttle, An Overview of synchronous Message-Passing and Topology, Electronic Notes Theor.Comput.Sci.39 (2000), no.2.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"8_CR30","volume-title":"Mathematical Studies","author":"P.J. Higgins","year":"1971","unstructured":"P.J. Higgins, Categories and Groupoids, Mathematical Studies,vol.32,van Nortrand Reinhold, London,1971."},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"G. Holzmann.On-the-fly model checking.ACM Computing Surveys, 28(4es):120\u2013120, December 1996.","DOI":"10.1145\/242224.242379"},{"key":"8_CR32","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0196-6774(81)90023-7","volume":"2","author":"W. Lipski","year":"1981","unstructured":"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\u2013226.","journal-title":"Journal of Algorithms"},{"key":"8_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for he working mathematician","author":"S. M. Lane","year":"1971","unstructured":"S. Mac Lane, Categories for he working mathematician, Graduate Texts in Mathematics, vol.5, Springer-Verlag, New York, Heidelberg, Berlin, 1971."},{"key":"8_CR34","series-title":"Lect Notes Comput Sci","first-page":"279","volume-title":"Petri Nets: Applications and Relationship to Other Models of Concurrency, Advances in Petri Nets 1986, PART II, PO of an Advanced Course","author":"A. Mazurkiewicz","year":"1986","unstructured":"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\u2013324, Bad Honnefs, September 1986. Springer-Verlag."},{"key":"8_CR35","unstructured":"J.R. Munkres, Elements of Algebraic Topology, Addison-Wesley,1984."},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"V. Pratt, Modelling concurrency with geometry, Proc.of the 18th ACM Symposium on Principles of Programming Languages.(1991).","DOI":"10.1145\/99583.99625"},{"issue":"4","key":"8_CR37","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1017\/S0960129500003145","volume":"10","author":"M. Raussen","year":"2000","unstructured":"M. Raussen, On the classification of dipaths in geometric models for concurrency, Math.Structures Comput.Sci.10 (2000), no.4, 427\u2013457.","journal-title":"Math.Structures Comput.Sci"},{"key":"8_CR38","unstructured":"-, State spaces and dipaths up to dihomotopy, Tech.Report R-01-2025, Department of Mathematical Sciences, Aalborg University, DK-9220 Aalborg \u00d8st, November 2001."},{"key":"8_CR39","unstructured":"V. Sassone and G.L. Cattani. Higher-dimensional transition systems. In Proceedings of LICS\u2019 96, 1996."},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"V. Sassone, M. Nielsen, and G. Winskel. Relationships between models of concurrency. In Proceedings of he Rex\u2019 93 school and symposium, 1994.","DOI":"10.1007\/3-540-58043-3_25"},{"issue":"2","key":"8_CR41","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2307\/1969485","volume":"54","author":"J.P. Serre","year":"1951","unstructured":"J.P. Serre, Homologie singuli\u00e8re des espaces fibr\u00e9s., Ann.of Math.(2) 54 (1951), 425\u2013505.","journal-title":"Ann.of Math."},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"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\u2013235, Santa Monica,California,Oct 1970.IEEE.","DOI":"10.1109\/SWAT.1970.20"},{"key":"8_CR43","unstructured":"S. Soko\u0142owski, 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\u2019 01 (Aalborg,Denmark) (P. Cousot et al.,ed.), vol. NS-01, BRICS Notes Series, no.7, BRICS, 2001, pp.77\u201397."},{"key":"8_CR44","unstructured":"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\u2013291."},{"issue":"3","key":"8_CR45","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0304-3975(89)90050-9","volume":"64","author":"Eugene W. Stark","year":"1989","unstructured":"A. Stark.Concurrent transition systems.Theoretical Computer Science, 64:221\u2013269, 1989.","journal-title":"Theoretical Computer Science"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"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\u201341.","DOI":"10.1090\/dimacs\/003\/04"},{"key":"8_CR47","unstructured":"R. van Glabbeek, Bisimulation semantics for higher dimensional automata, Tech. report, Stanford University,1991."},{"key":"8_CR48","unstructured":"R. van Glabbeek and U Goltz. Partial order semantics for refinement of actions. Bulle in of he EATCS, (34), 1989."},{"key":"8_CR49","series-title":"Lect Notes Comput Sci","volume-title":"Covering step graph","author":"F. Vernadat","year":"1996","unstructured":"F. Vernadat, P. Azema, and F. Michel. Covering step graph.Lecture Notes in Computer Science, 1091, 1996."},{"key":"8_CR50","doi-asserted-by":"crossref","unstructured":"G. Winskel and M. Nielsen. Models for concurrency, volume 3 of Handbook of Logic in Computer Science.Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198537809.003.0001"}],"container-title":["Lecture Notes in Computer Science","LATIN 2002: Theoretical Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45995-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,14]],"date-time":"2024-02-14T16:28:26Z","timestamp":1707928106000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45995-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434009","9783540459958"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/3-540-45995-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]}}}