{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T21:16:55Z","timestamp":1765228615717,"version":"3.46.0"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Polish National Center for Research and Luxembourg National Research Fund","award":["POLLUX-XI\/14\/SpaceVote\/2023","POLLUX-XI\/14\/SpaceVote\/2023"],"award-info":[{"award-number":["POLLUX-XI\/14\/SpaceVote\/2023","POLLUX-XI\/14\/SpaceVote\/2023"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Nat Comput"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Reaction systems are a model of computation inspired by the biochemistry exhibited by living cells. This paper introduces the notion of agency as an extension to the reaction systems formalism, leading to\n                    <jats:italic>distributed<\/jats:italic>\n                    reaction systems. Adding agents in the reaction systems setting, allows for the natural modelling and representation of multi-agent and distributed systems. To support the specification of temporal-epistemic properties of distributed reaction systems, we introduce the logic rs\n                    <jats:sc>ctlk<\/jats:sc>\n                    \u00a0and present experimental results of its associated model checking procedure run on a biological benchmark of within-cell signal transduction networks. The experimental results are encouraging despite the complexity of the rs\n                    <jats:sc>ctlk<\/jats:sc>\n                    \u00a0 model checking problem that is shown to be\n                    <jats:sc>pspace<\/jats:sc>\n                    -complete.\n                  <\/jats:p>","DOI":"10.1007\/s11047-025-10044-7","type":"journal-article","created":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T15:39:10Z","timestamp":1762357150000},"page":"1101-1117","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model checking for distributed reaction systems with temporal-epistemic properties"],"prefix":"10.1007","volume":"24","author":[{"given":"Artur","family":"Meski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maciej","family":"Koutny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u0141ukasz","family":"Mikulski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ion","family":"Petre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wojciech","family":"Penczek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcin","family":"Piatkowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,5]]},"reference":[{"key":"10044_CR1","doi-asserted-by":"crossref","unstructured":"Azimi S, Gratie C, Ivanov S, Petre I (2015a) Dependency graphs and mass conservation in reaction systems. Theoret Comput Sci 598:23\u201339","DOI":"10.1016\/j.tcs.2015.02.014"},{"key":"10044_CR2","unstructured":"Azimi S, Panchal C, Czeizler E, Petre I (2015b) Reaction systems models for the self-assembly of intermediate filaments. Ann Univ Bucharest LXI I(2):9\u201324"},{"key":"10044_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.tcs.2015.11.040","volume":"623","author":"S Azimi","year":"2016","unstructured":"Azimi S, Gratie C, Ivanov S, Manzoni L, Petre I, Porreca AE (2016) Complexity of model checking for reaction systems. Theoret Comput Sci 623:103\u2013113","journal-title":"Theoret Comput Sci"},{"key":"10044_CR4","doi-asserted-by":"crossref","unstructured":"Bowles J, Brodo L, Bruni R, Falaschi M, Gori R, Milazzo P (2024) Enhancing reaction systems with guards for analysing comorbidity treatment strategies. In: International conference on computational methods in systems biology. Springer, pp 27\u201344","DOI":"10.1007\/978-3-031-71671-3_3"},{"key":"10044_CR5","doi-asserted-by":"crossref","unstructured":"Brijder R, Ehrenfeucht A, Rozenberg G (2011) Reaction systems with duration. In: Computation, cooperation, and life - essays dedicated to gheorghe p\u0103un on the occasion of his 60th birthday. LNCS, 6610, 191\u2013202. Springer","DOI":"10.1007\/978-3-642-20000-7_16"},{"key":"10044_CR6","doi-asserted-by":"crossref","unstructured":"Brodo L, Bruni R, Falaschi M (2023) Verification of reaction systems processes. In: Challenges of software verification. Springer, pp 243\u2013264","DOI":"10.1007\/978-981-19-9601-6_13"},{"key":"10044_CR7","doi-asserted-by":"crossref","unstructured":"Ciencialov\u00e1 L, Cienciala L, Csuhaj-Varj\u00fa E (2022) Languages of distributed reaction systems. In: International conference on machines, computations, and universality. Springer, pp 75\u201390","DOI":"10.1007\/978-3-031-13502-6_5"},{"key":"10044_CR8","first-page":"1","volume":"2023","author":"L Ciencialov\u00e1","year":"2023","unstructured":"Ciencialov\u00e1 L, Cienciala L, Csuhaj-Varj\u00fa E (2023) Language classes of extended distributed reaction systems. Int J Found Comput Sci 2023:1\u201324","journal-title":"Int J Found Comput Sci"},{"key":"10044_CR9","volume-title":"Model checking","author":"EM Clarke","year":"2021","unstructured":"Clarke EM, Grumberg O, Peled DA (2021) Model checking. MIT Press"},{"key":"10044_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.tcs.2012.04.003","volume":"454","author":"L Corolli","year":"2012","unstructured":"Corolli L, Maj C, Marini F, Besozzi D, Mauri G (2012) An excursion in reaction systems: From computer science to biology. Theoret Comput Sci 454:95\u2013108","journal-title":"Theoret Comput Sci"},{"key":"10044_CR11","doi-asserted-by":"crossref","unstructured":"Dennunzio A, Formenti E, Manzoni L (2014) Extremal combinatorics of reaction systems. In: International conference on language and automata theory and applications. Springer, pp 297\u2013307","DOI":"10.1007\/978-3-319-04921-2_24"},{"key":"10044_CR12","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.ic.2019.03.006","volume":"267","author":"A Dennunzio","year":"2019","unstructured":"Dennunzio A, Formenti E, Manzoni L, Porreca AE (2019) Complexity of the dynamics of reaction systems. Inf Comput 267:96\u2013109","journal-title":"Inf Comput"},{"key":"10044_CR13","doi-asserted-by":"crossref","unstructured":"Ehrenfeucht A, Rozenberg G (2007a) Events and modules in reaction systems. Theoret Comput Sci 376(1\u20132):3\u201316","DOI":"10.1016\/j.tcs.2007.01.008"},{"key":"10044_CR14","unstructured":"Ehrenfeucht A, Rozenberg G (2007b) Reaction systems. Fund Inform 75(1\u20134):263\u2013280"},{"issue":"4\u20135","key":"10044_CR15","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1016\/j.tcs.2008.09.043","volume":"410","author":"A Ehrenfeucht","year":"2009","unstructured":"Ehrenfeucht A, Rozenberg G (2009) Introducing time in reaction systems. Theoret Comput Sci 410(4\u20135):310\u2013322","journal-title":"Theoret Comput Sci"},{"issue":"03","key":"10044_CR16","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1142\/S0129054110007295","volume":"21","author":"A Ehrenfeucht","year":"2010","unstructured":"Ehrenfeucht A, Main M, Rozenberg G (2010) Combinatorics of life and death for reaction systems. Int J Found Comput Sci 21(03):345\u2013356","journal-title":"Int J Found Comput Sci"},{"issue":"1","key":"10044_CR17","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1142\/S0129054111007927","volume":"22","author":"A Ehrenfeucht","year":"2011","unstructured":"Ehrenfeucht A, Main MG, Rozenberg G (2011) Functions defined by reaction systems. Int J Found Comput Sci 22(1):167\u2013178","journal-title":"Int J Found Comput Sci"},{"key":"10044_CR18","doi-asserted-by":"crossref","unstructured":"Ehrenfeucht A, Kleijn J, Koutny M, Rozenberg G (2013) Reaction systems: a natural computing approach to the functioning of living cells. In: A computable universe: understanding and exploring nature as computation. World Scientific, pp 189\u2013208","DOI":"10.1142\/9789814374309_0010"},{"key":"10044_CR19","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2016.12.031","volume":"682","author":"A Ehrenfeucht","year":"2017","unstructured":"Ehrenfeucht A, Kleijn J, Koutny M, Rozenberg G (2017) Evolving reaction systems. Theoret Comput Sci 682:79\u201399","journal-title":"Theoret Comput Sci"},{"issue":"1","key":"10044_CR20","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson EA, Halpern JY (1986) \u201cSometimes\u2019\u2019 and \u201cNot Never\u2019\u2019 revisited: on branching versus linear time temporal logic. J ACM 33(1):151\u2013178","journal-title":"J ACM"},{"key":"10044_CR21","volume-title":"Reasoning about knowledge","author":"R Fagin","year":"2003","unstructured":"Fagin R, Halpern JY, Moses Y, Vardi MY (2003) Reasoning about knowledge. MIT Press, Cambridge"},{"key":"10044_CR22","unstructured":"Ferrando A, Malvone V (2021) Towards the verification of strategic properties in multi-agent systems with imperfect information. Preprint at http:\/\/arxiv.org\/abs\/2112.13621"},{"key":"10044_CR23","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.tcs.2017.05.019","volume":"701","author":"D Genova","year":"2017","unstructured":"Genova D, Hoogeboom HJ, Jonoska N (2017) A graph isomorphism condition and equivalence of reaction systems. Theoret Comput Sci 701:109\u2013119","journal-title":"Theoret Comput Sci"},{"key":"10044_CR24","unstructured":"Jones AV, Knapik M, Penczek W, Lomuscio A (2012) Group synthesis for parametric temporal-epistemic logic. In: International conference on autonomous agents and multiagent systems, AAMAS 2012, Valencia, Spain, June 4-8, 2012 (3 Volumes), pp 1107\u20131114"},{"issue":"10","key":"10044_CR25","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1145\/1400181.1400200","volume":"51","author":"L Kari","year":"2008","unstructured":"Kari L, Rozenberg G (2008) The many facets of natural computing. Commun ACM 51(10):72\u201383","journal-title":"Commun ACM"},{"key":"10044_CR26","unstructured":"Kleijn J, Koutny M, Rozenberg G (2011) Modelling reaction systems with Petri nets. In: International workshop on biological processes & petri nets (BioPPN-2011)"},{"key":"10044_CR27","unstructured":"Lehninger AL (1965) Bioenergetics: the molecular basis of biological energy transformations. Biology teaching monograph series. W. A. Benjamin"},{"key":"10044_CR28","doi-asserted-by":"crossref","unstructured":"Lomuscio A, Ryan M (1997) On the relation between interpreted systems and Kripke models. In: Agents and multi-agent systems formalisms, methodologies, and applications. Lecture notes in artificial intelligence, vol 1441, Springer, pp 46\u201359","DOI":"10.1007\/BFb0055019"},{"issue":"1","key":"10044_CR29","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"Lomuscio A, Qu H, Raimondi F (2017) MCMAS: an open-source model checker for the verification of multi-agent systems. Int J Softw Tools Technol Transfer 19(1):9\u201330","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"4","key":"10044_CR30","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/s10472-023-09852-3","volume":"91","author":"B Maubert","year":"2023","unstructured":"Maubert B, Murano A, Rubin S (2023) Logical aspects of multi-agent systems. Ann Math Artif Intell 91(4):373\u2013374","journal-title":"Ann Math Artif Intell"},{"issue":"1","key":"10044_CR31","doi-asserted-by":"publisher","first-page":"70027","DOI":"10.1111\/ele.70027","volume":"28","author":"OJ Meacock","year":"2025","unstructured":"Meacock OJ, Mitri S (2025) Environment-organism feedbacks drive changes in ecological interactions. Ecol Lett 28(1):70027","journal-title":"Ecol Lett"},{"issue":"4","key":"10044_CR32","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/s10458-013-9232-2","volume":"28","author":"A M\u0119ski","year":"2014","unstructured":"M\u0119ski A, Penczek W, Szreter M, Wo\u017ana-Szcze\u015bniak B, Zbrzezny A (2014) BDD- versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Auton Agent Multi-Agent Syst 28(4):558\u2013604","journal-title":"Auton Agent Multi-Agent Syst"},{"key":"10044_CR33","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.ins.2015.03.048","volume":"313","author":"A M\u0119ski","year":"2015","unstructured":"M\u0119ski A, Penczek W, Rozenberg G (2015) Model checking temporal properties of reaction systems. Inf Sci 313:22\u201342","journal-title":"Inf Sci"},{"key":"10044_CR34","doi-asserted-by":"crossref","unstructured":"M\u0119ski A, Koutny M, Penczek W (2016) Towards quantitative verification of reaction systems. In: Unconventional Computation and Natural Computation: 15th International Conference, UCNC 2016, Manchester, UK, July 11-15, 2016, Proceedings, 142\u2013154","DOI":"10.1007\/978-3-319-41312-9_12"},{"issue":"1\u20134","key":"10044_CR35","doi-asserted-by":"publisher","first-page":"289","DOI":"10.3233\/FI-2017-1567","volume":"154","author":"A M\u0119ski","year":"2017","unstructured":"M\u0119ski A, Koutny M, Penczek W (2017) Verification of linear-time temporal properties for reaction systems with discrete concentrations. Fundam Inform 154(1\u20134):289\u2013306","journal-title":"Fundam Inform"},{"key":"10044_CR36","doi-asserted-by":"crossref","unstructured":"M\u0119ski A, Koutny M, Penczek W (2018) Reaction mining for reaction systems. In: Unconventional computation and natural computation - 17th international conference, UCNC 2018, Fontainebleau, France, June 25\u201329, 2018, Proceedings, pp 131\u2013144","DOI":"10.1007\/978-3-319-92435-9_10"},{"key":"10044_CR37","unstructured":"M\u0119ski A. Koutny M, Penczek W (2019) Model checking for temporal-epistemic properties of distributed reaction systems. Technical Report CS-TR-1526, School of Computing, Newcastle University, Newcastle upon Tyne, UK"},{"issue":"1","key":"10044_CR38","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1023\/A:1026181001368","volume":"75","author":"R Meyden","year":"2003","unstructured":"Meyden R, Wong K-S (2003) Complete axiomatizations for reasoning about knowledge and branching time. Stud Logica 75(1):93\u2013123","journal-title":"Stud Logica"},{"key":"10044_CR39","unstructured":"Panda S, Somenzi F (1995) Who are the variables in your neighborhood. In: Proceedings of the 1995 IEEE\/ACM international conference on computer-aided design, ICCAD 1995, San Jose, California, USA, November 5-9, 1995, 74\u201377"},{"key":"10044_CR40","doi-asserted-by":"crossref","unstructured":"Penczek W, Lomuscio A (2003) Verifying epistemic properties of multi-agent systems via bounded model checking. In: Proceedings of the second international joint conference on autonomous agents and multiagent systems. AAMAS \u201903. ACM, New York, pp 209\u2013216","DOI":"10.1145\/860575.860609"},{"key":"10044_CR41","doi-asserted-by":"crossref","unstructured":"Raimondi F, Lomuscio A (2004) Automatic verification of deontic interpreted systems by model checking via OBDD\u2019s. In: M\u00e1ntaras RL, Saitta L (eds.) Proceedings of ECAI, pp 53\u201357","DOI":"10.1007\/978-3-540-25927-5_15"},{"key":"10044_CR42","doi-asserted-by":"crossref","unstructured":"Raimondi F, Lomuscio A (2005) Symbolic model checking of multi-agent systems using OBDDs. In: Proc. of the 3rd NASA workshop on formal approaches to agent-based systems (FAABS III), Volume 3228 of LNCS. Springer, Cham, pp 213\u2013221","DOI":"10.1007\/978-3-540-30960-4_14"},{"volume-title":"Handbook of natural computing","year":"2012","key":"10044_CR43","unstructured":"Rozenberg G, B\u00e4ck T, Kok JN (eds) (2012) Handbook of natural computing. Springer, Cham"},{"issue":"01","key":"10044_CR44","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1142\/S0129054113500044","volume":"24","author":"A Salomaa","year":"2013","unstructured":"Salomaa A (2013) Functional constructions between reaction systems and propositional logic. Int J Found Comput Sci 24(01):147\u2013159","journal-title":"Int J Found Comput Sci"},{"key":"10044_CR45","unstructured":"Somenzi F (2009) CUDD: CU decision diagram package-release 2.4.0, vol 21, University of Colorado at Boulder"},{"key":"10044_CR46","volume-title":"An introduction to multi-agent systems","author":"M Wooldridge","year":"2002","unstructured":"Wooldridge M (2002) An introduction to multi-agent systems. Wiley, England"},{"issue":"1","key":"10044_CR47","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1186\/s41236-017-0004-9","volume":"1","author":"JGT Za\u00f1udo","year":"2017","unstructured":"Za\u00f1udo JGT, Scaltriti M, Albert R (2017) A network modeling approach to elucidate drug resistance mechanisms and predict combinatorial drug treatments in breast cancer. Cancer Converg 1(1):1\u201325","journal-title":"Cancer Converg"}],"container-title":["Natural Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11047-025-10044-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11047-025-10044-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11047-025-10044-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T18:44:07Z","timestamp":1765219447000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11047-025-10044-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,5]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["10044"],"URL":"https:\/\/doi.org\/10.1007\/s11047-025-10044-7","relation":{},"ISSN":["1567-7818","1572-9796"],"issn-type":[{"type":"print","value":"1567-7818"},{"type":"electronic","value":"1572-9796"}],"subject":[],"published":{"date-parts":[[2025,11,5]]},"assertion":[{"value":"22 July 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 November 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}