{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T23:06:06Z","timestamp":1785366366340,"version":"3.55.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,8,1]],"date-time":"2014-08-01T00:00:00Z","timestamp":1406851200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,8]]},"abstract":"<jats:p>Barbed bisimilarity is a widely used behavioral equivalence for interactive systems: given a set of predicates (denoted \u201cbarbs\u201d and representing basic observations on states) and a set of contexts (representing the possible execution environments), two systems are deemed to be equivalent if they verify the same barbs whenever inserted inside any of the chosen contexts. Despite its flexibility and expressiveness, this definition of equivalence is unsatisfactory because often the quantification is over an infinite set of contexts, thus making barbed bisimilarity very hard to be verified.<\/jats:p>\n          <jats:p>Should a labeled operational semantics be available, more efficient observational equivalences might be adopted. To this end, a series of techniques has been proposed to derive labeled transition systems (LTSs) from unlabeled ones, the main example being Leifer and Milner\u2019s theory of reactive systems. The underlying intuition is that labels should be the \u201cminimal\u201d contexts that allow for a reduction step to be performed.<\/jats:p>\n          <jats:p>However, minimality is difficult to asses, whereas the set of \u201cintuitively\u201d correct labels is often easily devised by the ingenuity of the researcher. This article introduces a framework that characterizes (weak) barbed bisimilarity via LTSs whose labels are (not necessarily minimal) contexts. Differently from previous proposals, our theory does not depend on the way the labeled transitions are built but instead relies on a simple set-theoretical presentation for identifying those properties such an LTS should verify to (1) capture the barbed bisimilarities of the underlying system and (2) ensure that such bisimilarities are congruences.<\/jats:p>\n          <jats:p>Furthermore, we adopt suitable proof techniques to make feasible the verification of such properties. To provide a test-bed for our formalism, we instantiate it by addressing the semantics of the Mobile Ambients calculus, recasting its barbed bisimilarities via label-based behavioral equivalences.<\/jats:p>","DOI":"10.1145\/2631916","type":"journal-article","created":{"date-parts":[[2014,9,17]],"date-time":"2014-09-17T14:22:25Z","timestamp":1410963745000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["A General Theory of Barbs, Contexts, and Labels"],"prefix":"10.1145","volume":"15","author":[{"given":"Filippo","family":"Bonchi","sequence":"first","affiliation":[{"name":"ENS Lyon, Universit\u00e9 de Lyon, LIP (UMR 5668 CNRS ENS Lyon UCBL INRIA), France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fabio","family":"Gadducci","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Pisa, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giacoma Valentina","family":"Monreale","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Pisa, Pisa, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,9,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00223-5"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 14th International Conference on Foundations of Software Science and Computational Structures (FOSSACS\u201911)","volume":"6604","author":"Aristizabal Andres","unstructured":"Andres Aristizabal , Filippo Bonchi , Catuscia Palamidessi , Luis Pino , and Frank D. Valencia . 2011. Deriving labels and bisimilarity for concurrent constraint programming . In Proceedings of the 14th International Conference on Foundations of Software Science and Computational Structures (FOSSACS\u201911) . Lecture Notes in Computer Science , Vol. 6604 . Springer, 138--152. Andres Aristizabal, Filippo Bonchi, Catuscia Palamidessi, Luis Pino, and Frank D. Valencia. 2011. Deriving labels and bisimilarity for concurrent constraint programming. In Proceedings of the 14th International Conference on Foundations of Software Science and Computational Structures (FOSSACS\u201911). Lecture Notes in Computer Science, Vol. 6604. Springer, 138--152."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.10.005"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266671"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.06.014"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 6th Workshop on Structural Operational Semantics (SOS\u201909)","author":"Bonchi Filippo","unstructured":"Filippo Bonchi , Fabio Gadducci , and Giacoma V. Monreale . 2009d. On barbs and labels in reactive systems . In Proceedings of the 6th Workshop on Structural Operational Semantics (SOS\u201909) . 46--61. Filippo Bonchi, Fabio Gadducci, and Giacoma V. Monreale. 2009d. On barbs and labels in reactive systems. In Proceedings of the 6th Workshop on Structural Operational Semantics (SOS\u201909). 46--61."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_22"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792831"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.010"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_24"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00231-5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600569X"},{"key":"e_1_2_1_13_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP\u201998)","author":"Fournet C\u00e9dric","unstructured":"C\u00e9dric Fournet and Georges Gonthier . 1998. A hierarchy of equivalences for asynchronous calculi . In Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP\u201998) . Lecture Notes in Computer Science , Vol. 1443 . Springer , 844--855. C\u00e9dric Fournet and Georges Gonthier. 1998. A hierarchy of equivalences for asynchronous calculi. In Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP\u201998). Lecture Notes in Computer Science, Vol. 1443. Springer, 844--855."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37635-1_10"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28729-9_24"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11548133_2"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 11th International Conference on Concurrency Theory (CONCUR\u201900)","volume":"1877","author":"James","unstructured":"James J. Leifer and Robin Milner. 2000. Deriving bisimulation congruences for reactive systems . In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR\u201900) . Lecture Notes in Computer Science , Vol. 1877 . Springer, 243--258. James J. Leifer and Robin Milner. 2000. Deriving bisimulation congruences for reactive systems. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR\u201900). Lecture Notes in Computer Science, Vol. 1877. Springer, 243--258."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101825"},{"key":"e_1_2_1_19_1","volume-title":"Communication and Concurrency","author":"Milner Robin","unstructured":"Robin Milner . 1989. Communication and Concurrency . Prentice Hall , Upper Saddle River, NJ. Robin Milner. 1989. Communication and Concurrency. Prentice Hall, Upper Saddle River, NJ."},{"key":"e_1_2_1_20_1","volume-title":"Communicating and Mobile Systems: The &pi;-Calculus","author":"Milner Robin","unstructured":"Robin Milner . 1999. Communicating and Mobile Systems: The &pi;-Calculus . Cambridge University Press , Cambridge, MA . Robin Milner. 1999. Communicating and Mobile Systems: The &pi;-Calculus. Cambridge University Press, Cambridge, MA."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.07.003"},{"key":"e_1_2_1_22_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 19th International Colloquium on Automata, Languages, and Programming (ICALP\u201992)","author":"Milner Robin","unstructured":"Robin Milner and Davide Sangiorgi . 1992. Barbed bisimulation . In Proceedings of the 19th International Colloquium on Automata, Languages, and Programming (ICALP\u201992) . Lecture Notes in Computer Science , Vol. 623 . Springer , 685--695. Robin Milner and Davide Sangiorgi. 1992. Barbed bisimulation. In Proceedings of the 19th International Colloquium on Automata, Languages, and Programming (ICALP\u201992). Lecture Notes in Computer Science, Vol. 623. Springer, 685--695."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.005"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_36"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/941344.941349"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.40"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00309-1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631916","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2631916","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:19:13Z","timestamp":1750231153000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631916"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["10.1145\/2631916"],"URL":"https:\/\/doi.org\/10.1145\/2631916","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8]]},"assertion":[{"value":"2013-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}