{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T11:25:32Z","timestamp":1769513132694,"version":"3.49.0"},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,5,1]],"date-time":"2014-05-01T00:00:00Z","timestamp":1398902400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"},{"start":{"date-parts":[[2013,1,8]],"date-time":"2013-01-08T00:00:00Z","timestamp":1357603200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Stochastic bigraphical reactive systems (SBRS) is a recent formalism for modelling systems that evolve in time and space. However, the underlying spatial model is based on sets of trees and thus cannot represent spatial locations that are shared among several entities in a simple or intuitive way. We adopt an extension of the formalism,\n            <jats:italic>SBRS with sharing<\/jats:italic>\n            , in which the topology is modelled by a directed acyclic graph structure. We give an overview of SBRS with sharing, we extend it with rule priorities, and then use it to develop a model of the 802.11 CSMA\/CA RTS\/CTS protocol with exponential backoff, for an\n            <jats:italic>arbitrary<\/jats:italic>\n            network topology with possibly overlapping signals. The model uses sharing to model overlapping connectedness areas, instantaneous prioritised rules for deterministic computations, and stochastic rules with exponential reaction rates to model constant and uniformly distributed timeouts and constant transmission times. Equivalence classes of model states modulo instantaneous reactions yield states in a CTMC that can be analysed using the model checker PRISM. We illustrate the model on a simple example wireless network with three overlapping signals and we present some example quantitative properties.\n          <\/jats:p>","DOI":"10.1007\/s00165-012-0270-3","type":"journal-article","created":{"date-parts":[[2013,1,7]],"date-time":"2013-01-07T04:35:02Z","timestamp":1357533302000},"page":"537-561","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Modelling IEEE 802.11 CSMA\/CA RTS\/CTS with stochastic bigraphs with sharing"],"prefix":"10.1145","volume":"26","author":[{"given":"Muffy","family":"Calder","sequence":"first","affiliation":[{"name":"School of Computing Science, University of Glasgow, Lilybank Gardens, G12 8QQ, Glasgow, UK"}]},{"given":"Michele","family":"Sevegnani","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Lilybank Gardens, G12 8QQ, Glasgow, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Alshanyour A Agarwal A (2010) Performance of IEEE 802.11 RTS\/CTS with finite buffer and load in imperfect channels: modeling and analysis. In: GLOBECOM pp 1\u20136","DOI":"10.1109\/GLOCOM.2010.5684057"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Aziz A Sanwal K Singhal V Brayton R (1996) Verifying continuous time Markov chains. In: Alur R Henzinger T (eds) Computer aided verification. Lecture notes in computer science vol 1102. Springer Berlin-Heidelberg pp 269\u2013276","DOI":"10.1007\/3-540-61474-5_75"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90006-6"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/49.840210"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019109301754"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Clarke E (2008) The birth of model checking. In: Grumberg O Veith H (eds) 25 Years of model checking. Lecture notes in computer science vol 5000. Springer Berlin-Heidelberg pp 1\u201326","DOI":"10.1007\/978-3-540-69850-0_1"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Conforti G Macedonio D Sassone V (2005) Spatial logics for bigraphs. In: Caires L Italiano GF Monteiro L Palamidessi C Yung M (eds) Proceedings of the 32th international colloquium on automata languages and programming (ICALP\u201905). Lecture notes in computer science vol 3580. Springer Berlin pp 766\u2013778","DOI":"10.1007\/11523468_62"},{"key":"e_1_2_1_2_8_2","unstructured":"Calder M Sevegnani M (2012) Matching and rewriting for bigraphs with sharing. Submitted for publication"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.012"},{"key":"e_1_2_1_2_10_2","unstructured":"IEEE. (2005) Std. 802.11e-2005 Part 11: wireless LAN medium access control (MAC) and physical layer (PHY) specifications Amendment 8: medium access control (MAC) quality of service enhancements"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.006"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G Qadeer S (eds) Proceedings of 23rd international conference on computer aided verification (CAV\u201911). Lecture notes in computer science vol 6806. Springer Berlin pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Sproston J (2002) Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns H Segala R (eds) Proceedings of 2nd joint international workshop on process algebra and probabilistic methods performance modeling and verification (PAPM\/PROBMIV\u201902). Lecture notes in computer science vol 2399. Springer Berlin pp 169\u2013187","DOI":"10.1007\/3-540-45605-8_11"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/1540607"},{"key":"e_1_2_1_2_15_2","unstructured":"Sevegnani M Calder M (2010) Bigraphs with sharing. Technical report TR-2010-310 University of Glasgow"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0270-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-012-0270-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0270-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0270-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:57:19Z","timestamp":1641484639000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0270-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5]]},"references-count":15,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,5]]}},"alternative-id":["10.1007\/s00165-012-0270-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0270-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5]]},"assertion":[{"value":"23 July 2012","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 November 2012","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 November 2012","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2013","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}