{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:24Z","timestamp":1759638924631},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2008,7,1]],"date-time":"2008-07-01T00:00:00Z","timestamp":1214870400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Bisimulations are well-established behavioural equivalences that are widely used to study properties of computer science systems. Bisimulations assume the behaviour of systems to be described as labelled transition systems, and properties of a system can be verified by assessing its bisimilarity with a system one knows to enjoy those properties.<\/jats:p>\n          <jats:p>In this paper we show how semantics based on labelled transition systems and bisimulations can be defined for two formalisms for the description of biological systems, both capable of describing membrane interactions. These two formalisms are the Calculus of Looping Sequences (CLS) and Brane Calculi, and since they stem from two different approaches (rewrite systems and process calculi) bisimulation appears to be a good candidate as a general verification method.<\/jats:p>\n          <jats:p>We introduce CLS and define a labelled semantics and bisimulations for which we prove some congruence results. We show how bisimulations can be used to verify properties by way of two examples: the description of the regulation of lactose degradation in Escherichia coli and the description of the EGF signalling pathway. We recall the PEP calculus (the simplest of Brane Calculi) and its translation into CLS, we define a labelled semantics and some bisimulation congruences for PEP processes, and we prove that bisimilar PEP processes are translated into bisimilar CLS terms.<\/jats:p>","DOI":"10.1007\/s00165-008-0071-x","type":"journal-article","created":{"date-parts":[[2008,3,10]],"date-time":"2008-03-10T06:51:40Z","timestamp":1205131900000},"page":"351-377","source":"Crossref","is-referenced-by-count":21,"title":["Bisimulations in calculi modelling membranes"],"prefix":"10.1145","volume":"20","author":[{"given":"Roberto","family":"Barbuti","sequence":"first","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Pisa, Largo B. Pontecorvo 3, 56127, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Maggiolo-Schettini","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Pisa, Largo B. Pontecorvo 3, 56127, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paolo","family":"Milazzo","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Pisa, Largo B. Pontecorvo 3, 56127, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Troina","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Torino, Corso Svizzera 185, 10149, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Alur R Belta C Ivancic F Kumar V Mintz M Pappas GJ Rubin H Schug J (2001) Hybrid Modeling and Simulation of Biomolecular Networks. In: Proceedings of hybrid systems: computation and control LNCS 2034. Springer Heidelberg pp 19\u201332","DOI":"10.1007\/3-540-45351-2_6"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.03.064"},{"key":"e_1_2_1_2_3_2","first-page":"1","article-title":"A calculus of looping sequences for modelling microbiological systems","volume":"72","author":"Barbuti R","year":"2006","journal-title":"Fundam Inf"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barbuti R Maggiolo-Schettini A Milazzo P Troina A (2006) Bisimulation congruences in the calculus of looping sequences. In: Proceedeings of international colloquium on theoretical computer science (ICTAC\u201906) LNCS 4281. Springer Heidelberg pp 93\u2013107","DOI":"10.1007\/11921240_7"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Busi N (2006) Deciding behavioural properties in Brane Calculi. In: Proceedings of computational methods in systems biology (CMSB\u201906) LNBI 4210. Springer Heidelberg pp 17\u201331","DOI":"10.1007\/11885191_2"},{"key":"e_1_2_1_2_6_2","unstructured":"Busi N (2007) Towards a causal semantics for Brane Calculi. In: Proceedings of the fifth brainstorming week on membrane computing pp 97\u2013111"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cardelli L (2005) Brane Calculi. Interactions of Biological Membranes. In: Proceedings of computational methods in systems biology (CMSB\u201904) LNCS 3082. Springer Heidelberg pp 257\u2013280","DOI":"10.1007\/978-3-540-25974-9_24"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.03.063"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.03.066"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.03.065"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_2_12_2","unstructured":"Laneve C Tarissan F (2006) A simple calculus for proteins and cells. In: Proceedings of membrane computing and biologically inspired process calculi (MeCBIC\u201906)"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Leifer J Milner R (2000) Deriving bisimulation congruences for reactive systems. In: Proceedings of concurrency theory (CONCUR\u201900) LNCS 1877. Springer Heidelberg pp 243\u2013258","DOI":"10.1007\/3-540-44618-4_19"},{"key":"e_1_2_1_2_14_2","unstructured":"Matsuno H Doi A Nagasaki M Miyano S (2000) Hybrid petri net representation of gene regulatory network. In: Proceedings of pacific symposium on biocomputing. World Scientific Press pp 341\u2013352"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Miculan M Bacci G (2006) Modal logics for brane calculus. In: Proceedings of computational methods in systems biology (CMSB\u201906) LNBI 4210. Springer Heidelberg pp 1\u201316","DOI":"10.1007\/11885191_1"},{"key":"e_1_2_1_2_16_2","unstructured":"Milazzo P (2007) Qualitative and quantitative formal modeling of biological systems PhD Thesis University of Pisa"},{"key":"e_1_2_1_2_17_2","volume-title":"Communication and concurrency","author":"Milner R","year":"1989"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/329902"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Milner R Sangiorgi D (1992) Barbed bisimulation. In: Proceedings of international colloquium on automata Languages and Programming (ICALP\u201992) LNCS 623 pp 685\u2013695","DOI":"10.1007\/3-540-55719-9_114"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.compbiomed.2006.01.006"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Priami C Quaglia P (2005) Beta binders for biological interactions. In: Proceedings of computational methods in systems biology (CMSB\u201904) LNCS 3082. Springer Heidelberg pp 20\u201333","DOI":"10.1007\/978-3-540-25974-9_3"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.03.061"},{"key":"e_1_2_1_2_23_2","unstructured":"Regev A Silverman W Shapiro EY (2001) Representation and simulation of biochemical processes using the pi-calculus process algebra. In: Proceedings of Pacific symposium on biocomputing. World Scientific Press pp 459\u2013470"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0096"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00309-1"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","first-page":"4521","DOI":"10.1128\/jvi.67.8.4521-4532.1993","article-title":"The E5 oncoprotein of human papillomavirus type 16 transforms fibroblasts and effects the downregulation of the epidermal growth factor receptor in keratinocytes","volume":"67","author":"Straight SW","year":"1993","journal-title":"J Virol"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0959-8049(01)00230-1"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1038\/35052073"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"van Glabbeek RJ (1990) The linear time-branching time spectrum. In: Proceedings of international conference on concurrency theory (CONCUR\u201990) LNCS 458 pp 278\u2013297","DOI":"10.1007\/BFb0039066"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-008-0071-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-008-0071-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-008-0071-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:46:15Z","timestamp":1641483975000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-008-0071-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7]]},"references-count":29,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["10.1007\/s00165-008-0071-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-008-0071-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,7]]}}}